It is not a claim to have solved, or to be about to solve, a Millennium Problem, a famous Erdős problem, or a FrontierMath item. As of this writing the best-funded attempt at the FrontierMath Erdős benchmark (68 curated, still-open Erdős problems, formalised in Lean) solved 5 of 68 for over $220,000 in unconstrained compute, and every other model tested solved zero. That is the honest size of the gap between what current AI-assisted mathematics can do and what these problems ask. This book's ambition is scaled to match: identify real, checkable, modestly-scoped sub-questions where the corpus's existing proofs are genuinely load-bearing, not to shortcut that gap.
| § | the thread | the corpus anchor | status |
|---|---|---|---|
| 1 | Where the Ladder Runs Out — the Skolem Problem at order 5, and the n-bonacci ladder this corpus already named up to order 6 | NbonacciLadder.lean | open thread |
| 2 | The η that drifted — two of the author's own monographs stating the Tribonacci constant to different, incompatible precision, six months apart, and what it costs to notice | darkmatter_monograph_v2.pdf vs. dm3_gravitational_lensing_monograph.pdf | planned, not written |
| 3 | The Catalog Says No — Bloom's public catalog of 1,221 problems (593 open, 43 tags), matched mechanically against every proven lemma this corpus holds | erdos_catalog_crosscheck.py | run 2026-09-27 — 0 matches |
| 4 | Navier–Stokes | NavierStokesAndEuler (empty repo) | reserved, no content, no claim |
| 5 | Hodge conjecture | — | open; no corpus material touches it |
Every thread in this book carries three labels, checked before it is written and re-checked before anything is added to it: the open problem, cited to a primary source and dated; the corpus result, cited to a file and line, kernel-audited, not recalled; and the gap between them, stated in one sentence a specialist in the open problem would accept as accurate. A thread failing any of the three is a stub, not a chapter.
FrontierMath (Glazer et al., Epoch AI, arXiv:2411.04872) is a benchmark: expert-vetted, previously unpublished, automatically verifiable research-level problems, under 2% solved by 2024 frontier models. It is not itself a source of open problems for this book — its problems are already solved, with solutions held privately for benchmark integrity. What it is: a curated map of where genuine mathematical difficulty currently sits, by subject area, and the reason this book exists at all. FrontierMath Erdős, its sibling benchmark on 68 real still-open Erdős problems, is the closer source: those problems are actually open, and its published results are this book's honest baseline for what "hard" costs today.