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ₖ obey eₖ² C (n, k-1) C (n, k+1) ≥ e₊-₁ e₊+₁ C (n, k) ² for 1 ≤ k ≤ n-1; equivalently, the normalized means pₖ = eₖ / 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²-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ₖ 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.
CARLES MARÍN MUÑOZ (Sun,) studied this question.