Title: Three RH claims and one dataset with a commit SHA | MidnightDev
URL: https://midnightdev.dev/writing/rh-claim-and-the-sha
Description: August to October: two claimed proofs of the Riemann Hypothesis, one claimed weaker version, one podcast episode. What none of them can answer until someone runs them — and the local index of 205,597 machine-checked theorems that every line of this page cites.
Generated from the live page on 2026-10-27. Do not edit by hand; run `pnpm twins`.

---

01 / what landed

# Three claims, zero of them run yet

| date | who | claim | status |
| --- | --- | --- | --- |
| 2026-08 | Alpöge & Furman | Claimed proof of RH, argument from an unreleased Anthropic research model | claimed — not independently verified |
| 2026-10-06 | OpenAI | “quasi-RH” among 377 announced results; Quanta covered the batch on 10-19 | claimed — weaker statement, under review |
| 2026-10-27 | everyone | Lex Fridman №503: “AI Crisis in Math: Navier–Stokes, RH & Complexity Theory” | discussion — no new claim |

02 / why \u201cclaimed\u201d is doing work

## 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.

03 / what can be cited

## 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.

every claim in this page is reproducible

```
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.

04 / why it matters to me

## “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.

sources

- [Quanta — AI Proved the Quasi-Riemann Hypothesis (2026-10-19)](https://www.quantamagazine.org/ai-proved-the-quasi-riemann-hypothesis-what-happens-now-20261019/)
- [Anthropic — what the model produced on ζ](https://www.anthropic.com/research/riemann-zeta)
- [mathlib4 @8000f01 — the tree tonight’s index was cut from](https://github.com/leanprover-community/mathlib4/commit/8000f01d29bcdc39ff67a1a4248cc10adcf9ebb0)
- [RH, current state of the claims (Wikipedia)](https://en.wikipedia.org/wiki/Riemann_hypothesis)

[all writing](https://midnightdev.dev/writing.md)