Three claims, zero of them run yet

A proof that has not been run is a claim with extra steps

RH is special precisely because the object has a formal definition sitting inside Lean’s math library tonight: Mathlib/NumberTheory/LSeries/RiemannZeta.lean:185 — def Mathlib.RiemannHypothesis : Prop. Which means every “proof of RH” has somewhere to be checked, and until someone feeds the argument to a kernel and gets : RiemannHypothesis, the honest word for it is “claimed.”

Every article published today about today’s episode quotes the same three paragraphs and stops. That is also its distinguishing feature: none of them can point at a single machine-checked object inside their text.

205,597 theorems, one commit SHA, one grep

So tonight’s page cites things instead of vibes. On disk, cut from today’s master tree (@8000f01): an index of every theorem, lemma, class and structure in mathlib4 — 8,662 files scanned, 205,597 declarations, 204,119 unique names, each row carrying its fully qualified name, source file and line.

grep ',det_mul,' mathlib4-index.csv
# -> theorem,Mathlib.Matrix.det_mul,Mathlib/LinearAlgebra/Matrix/
#    Determinant/Basic.lean,141,...

Whatever the RH verdict turns out to be, that file is a standing citation target: a news story that quotes a theorem ID plus a commit SHA is checkable by anyone, forever, with one command.

“Expected: not 10X.” He said: a million X.

Tonight’s episode includes a line that will stick around — Kontorovich on going from handwriting Lean to a model that finds the lemma you need without knowing its name: “he expected X, not ten X; it felt like a million X.” The tooling bullet on the slide is the part this site runs on: the dataset is a running instance of exactly that “library search,” and the case-study file already has a dated, SHA-stamped exhibit for it instead of another paragraph of capability prose.