The Inward Bow of a Real-Rooted Polynomial: Newton's Inequalities, Machine-Checked in Lean 4
CARLES MARÍN MUÑOZ · Zenodo (CERN European Organization for Nuclear Research) · 2026
A machine-checked, sorry-free proof, in Lean 4 over Mathlib, of Newton's inequalities (1707): if a real polynomial of degree n has all real roots, its elementary symmetric functions e_k obey e_k^2 C(n,k-1) C(n,k+1) ≥ e_{k-1} e_{k+1} C(n,k)^2 for 1 ≤ k ≤ n-1; equivalently, the normalized means p_k = e_k / C(n,k) are log-concave. This is the classical bridge real-rooted ⇒ log-concave, the elementary base beneath the matching polynomial, the Heilmann–Lieb theorem, and the Hodge-theoretic proofs of matroid log-concavity. Mathlib already carried the elementary symmetric functions (Multiset.esymm) and the Vieta relations; it did not carry the inequality, and to the best of the author's knowledge no proof assistant did. The proof is the classical reduction made fully rigorous: real-rootedness survives differentiation (Rolle) and reversal (x → 1/x), so differentiating i-1 times, reversing, and differentiating again collapses the k-th instance to a real-rooted quadratic, whose discriminant b^2-4ac ≥ 0 is the inequality once positive factorials are cleared. The symmetric-function form is machine-checked for monic polynomials (no loss, since the e_k depend only on the roots); the coefficient form is checked with no normalization. The headline theorems depend only on the three standard axioms (propext, Classical.choice, Quot.sound). Lean source: Newton.lean in the repository. Toolchain v4.30.0-rc2, Mathlib pin 701fb6e9. Includes the English and Spanish versions of the paper and the Lean source file.