Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Semi-Algebraic Lean • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can a machine decide whether a system of polynomial inequalities has a real solution? Yes — Tarski proved in 1951 that the first-order theory of the reals is decidable. This project formalizes the decision procedure in Lean 4: given a quantifier-free system of polynomial constraints over ℜ, it either finds a satisfying point or produces a Positivstellensatz refutation proving no solution exists. The machinery — cylindrical algebraic decomposition, Sturm chains, sign determination — is all machine-checked.
Key Verified Results
tarski_decidableFirst-order theory of reals is decidable
Decidability.lean
cad_correctCAD decomposes ℝⁿ into sign-invariant cells
CAD.lean
sat_certificate_soundSAT witness satisfies all constraints
Certificate.lean
unsat_certificate_soundPositivstellensatz refutation proves infeasibility
Certificate.lean