Open Research Index

sneed-and-feed/lean-theorems-1

Sneed & Feed Formalization Team

Palomar Registrypalomar/PALOMAR-2026-08-27-000016Aug 27, 2026math.AGscore 0

A complete machine-checked Lean 4 formalization of Descartes's Rule of Signs (1637, Wiedijk #73). Proves that for any non-zero real polynomial p(X) over ℝ, the number of positive real roots counted with algebraic multiplicity is bounded above by the number of sign variations in its coefficient sequence (ignoring zero coefficients), and their difference is an even non-negative integer. While the pinned Mathlib revision (Mathlib v4.34.0-rc1) contains the upper-bound inequality in `Mathlib.Algebra.Polynomial.RuleOfSigns` (`Polynomial.roots_countP_pos_le_signVariations`), this development…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000016
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000016/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000016/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'