Validated numerics

Summary

Validated numerics, also called verified or rigorous computation, is numerical computation whose output comes with a mathematical guarantee. Instead of a single approximate number, it returns a set, usually an interval or a box, that provably contains the exact answer. All round-off errors and truncation errors are bounded, typically with interval arithmetic or affine arithmetic and directed rounding. Its results can serve as steps of a proof; an example is Warwick Tucker's computer-assisted proof that the Lorenz attractor exists.