The Staircase of Signs: Sturm's Root-Counting Theorem, Machine-Checked in Lean 4

Abstract

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 native_decide 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.