Here’s an example using GitHub - JuliaIntervals/IntervalArithmetic.jl: Rigorous floating-point calculations using interval arithmetic in Julia.
The main method / goal of interval arithmetic is to calculate the range of a function f over an input set X, i.e. the set \mathcal{R}(f; X) := \{f(x): x \in X \}. Calculating this exactly is hard (impossible in general, equivalent to global optimisation of the function), but interval arithmetic gives a cheap way of calculating an enclosure Y of this range, i.e. an interval that is guaranteed to contain it: \mathcal{R}(f; X) \subseteq Y.
The idea is to split up a complicated function f into simple pieces and make sure you bound the range for each piece. Putting the pieces together gives you an enclosure for the complicated function (the “fundamental theorem of interval arithmetic”), but which is in general an over-estimate.
julia> using IntervalArithmetic
julia> f(x) = x * exp(x)
f (generic function with 1 method)
julia> X = interval(1, 2)
[1, 2]
julia> f(X)
[2.71828, 14.7782]
julia> f(X).lo > 0
true
This constitutes a rigorous proof that f(x) > 0 for all x \in X, where X = [1, 2] is the interval of all real numbers between 1 and 2.
In fact you can also do things like
julia> f(0..∞)
[0, ∞]
to prove this for any x \ge 0!
But this technique has “some” (many) limitations, where it can’t prove things that you know to be true, for example
julia> g(x) = x^2 - 2x
julia> g(100..∞)
[-∞, ∞]
This just says that the true range of the function over that input set is contained in (i.e. is a subset of) the given result.
In this case we (humans) actually know that x^2 is much bigger than 2x in that interval, and hence the function is positive there. In this particular case you could deduce that by calculating the derivative, e.g. using ForwardDiff.jl
(which works out of the box with intervals!). But in general I believe it is a hard problem. (But I am very willing to be proved wrong here!)