// the find
teorth/estimates
Code to automatically prove or verify estimates in analysis
A lightweight Python proof assistant from Terence Tao's team for verifying inequalities and asymptotic estimates, not full theorems. It's for people doing analysis who want Lean-style tactic proofs (cases, linarith, simp) for tedious inequality chasing without the overhead of a real proof assistant like Lean or Isabelle.
Linarith uses exact linear programming instead of floating point, so it won't produce false positives from rounding and gives an actual numeric counterexample when a goal is false rather than just failing silently. Tactic mode mirrors Lean's structure closely (branching proof tree, verbose mode explaining each step) which makes the output legible instead of a black box. It's built on sympy, so you get full symbolic manipulation for free alongside the tactic framework, and there's a browser-based UI (Pyodide + visual proof tree) so people can try it with zero install.
The lemma library is explicitly unfinished per the README ('I plan to build...') — right now it's a handful of lemmas like AM-GM and some Littlewood-Paley support, so anything beyond linear arithmetic and a few special cases needs hand-rolled tactics. Scope is narrow by design: it only handles estimate/inequality-style goals, not general theorem proving, so it's a companion tool rather than a Lean replacement. Install instructions point at `uvx --with git+https://github.com/...` off the default branch rather than a pinned release or PyPI package, which is a reproducibility risk if the API shifts under you. The repo bundles large generated WASM/JS blobs (z3-built.wasm, prebuilt wheels) directly in ui/public instead of fetching them at build time, which bloats the repo and can silently go stale against the core Python package.