A machine-checked, sorry-free formalization, in Lean 4 over Mathlib, of Sturm's theorem (1829): for a squarefree real polynomial p and an interval (a, b] whose endpoints are not roots, the number of distinct real roots of p in (a, b] equals V (a) − V (b), where V (x) is the number of sign changes of the Sturm sequence p, p′, − (p mod p′), … evaluated at x (zeros discarded). No root is ever located; two integers are subtracted. The mathematics is entirely classical and the result has been formalized before in other systems (Coq, by Cohen, within the construction of the real algebraic numbers; Isabelle/HOL, by Eberl, and in the Sturm–Tarski form by Li and Paulson; and HOL Light). To the best of the author's knowledge — based on searches of Loogle and Mathlib in June 2026 — this is the first proof of Sturm's theorem in Lean; it is a first-in-Lean and not a first-in-any-system. The contribution is therefore the formalization itself together with its reusable machinery: a small theory of sign variation, an inductive flank-reduction relation (FlankReduce) that decouples the chain's combinatorics from its algebra, and the local-to-global passage from a single root crossing to the interval count. A by-product is that Mathlib's existing count of coefficient sign variations (Descartes' rule, Polynomial. signVariations) and the count used here are, after unfolding, the same function — so the toolkit transfers verbatim to Descartes. The headline theorem Sturm. sturm depends only on the three standard axioms propext, Classical. choice, Quot. sound; no nativedecide and no custom axiom. The whole proof is a single file (Sturm. lean, about 1, 220 lines, ~60 declarations) depending on Mathlib alone. Scope, stated plainly: the theorem is proved for squarefree p over the reals; the passage to p/gcd (p, p′) for arbitrary polynomials is not formalized here. English and Spanish editions are included. Formalized with AI assistance (Claude, Anthropic) ; the mathematics and all claims are the author's responsibility, and the Lean kernel — not the assistant — certifies the proofs.
CARLES MARÍN MUÑOZ (Mon,) studied this question.