Peter Tallosy

Mainly to make it possible to formalize physics problems in Lean with differential equations which very often have solutions involving transcendental functions (like sin() or cos() for the harmonic oscillator, or the Schrödinger equation with very simple boundary conditions, though those can be written as a complex exponential exp(i*x), or log() for rocket equations, etc.) or some composition of them.

Lean tactics that prove bounds on exp, log, sin and cos in Mathlib, for goals like a < Real.exp r. They use a Taylor polynomial plus a remainder you can bound (Taylor–Lagrange interval bounds, so the true value sits between two explicit rational numbers). There is an approx tactic and a norm_num extension.

If the tactic closes the goal, the Lean kernel (the small verifier that only accepts valid proof steps) has checked it. I only used exact rational arithmetic (no floating point or native_decide == no untrusted numeric code outside the checker).