Here’s an example using https://github.com/JuliaIntervals/IntervalArithmetic.jl.

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!)