AI Proved What?

AN02 (outside OpenAI’s math catalogue), October 2026

Two thirds of the zeta zeros, simple and on the line?

A result first found by Claude, checked by its two authors at Anthropic (not independently reviewed), proved again by Lamzouri, and formalized in Lean

Disclosure. AI Proved What? is made with Claude, Anthropic’s AI. This is Anthropic’s own result: we hold it to the same standards as every other lab’s, using only public sources. AI Proved What? is independent and not affiliated with Anthropic beyond using its product Claude, and not affiliated with Axiom.

8:11. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:42The claim
  3. 4:03How the proof goes
  4. 6:11Where it stands

The claim, in plain words

Episode AN02 covers a result in three public documents. On August 10, 2026, Anthropic posted that an unreleased research version of Claude had improved a lower bound for the share of zeros on the line. On August 13, a preprint followed on arXiv, listing Levent Alpöge and Ralph Furman as authors. Its first page says: the mathematical argument in this paper was discovered and written by Claude, an AI developed by Anthropic. The listed authors verified the proof and take responsibility for its content. The theorem: unconditionally, as the height grows, at least two thirds of the zeros, counted with multiplicity, are simple and on the line, and at least five sixths are distinct. With Montgomery and Taylor’s window, the constants become 67.25% and 83.62%; the first is the number Montgomery and Taylor had reached assuming the Riemann hypothesis.

The third document is Lamzouri’s. On September 2, Youness Lamzouri, of the University of Lorraine, posted what he calls a new, conceptually simpler proof of the same two bounds. A revision on September 8 added two estimates of his own: at least 88.76% of the zeros are simple or on the line. His abstract says the first proof was produced by an internal research version of Claude developed by Anthropic and subsequently verified by two mathematicians at Anthropic, Levent Alpöge and Ralph Furman, and that his additional estimates are neither stated nor proved in the Claude paper. He calls it a breakthrough result, and says the argument produced by Claude is technically intricate, and its main mechanism is not immediately transparent.

What it doesn’t claim

What is not claimed. Not the Riemann hypothesis: Claude’s paper says the remaining third of the zeros are not shown to be off the line, merely not reached. Not that every zero is simple. These are limits as the height grows, not statements about any one zero. Anthropic’s post says: we don’t expect that the techniques Claude used will lead to proving the Riemann hypothesis. The paper says the Riemann hypothesis itself is out of reach of the mechanism, and puts the ceiling for certificates of this type near 68.2%, a bound worked out by Eric Easley and Stephen McAleer.

Where it stands

Preprints on arXiv
Alpöge and Furman, arXiv 2608.13637: August 13, 2026 (v2 August 19); Lamzouri, arXiv 2609.02882: September 2, 2026 (v2 September 8); Anthropic’s post: August 10, 2026
Journal publication
None yet. Anthropic’s repository metadata says “journal peer review is pending”; neither arXiv record has a journal reference
Independent expert review
None named in our sources. The proof was checked by Levent Alpöge and Ralph Furman, mathematicians at Anthropic (the listed authors): they “read the argument in detail”, checked it, condensed it to the form in which it appears, and “take responsibility for any errors that remain” (the paper). Brian Conrey and Daniel Goldston are thanked “for carefully reading the manuscript and for their comments” (the paper); Anthropic’s post says they “examined the paper on short notice”. No source says they verified or endorsed it. Anthropic’s Lean metadata says the paper was “reviewed and endorsed by a human analytic number theorist”, not named; the paper thanks “colleagues at Anthropic who carried out additional independent reviews”, not named
A second proof
Youness Lamzouri (Université de Lorraine), by a different route, with two further estimates of his own
Lean, by Anthropic and by Axiom
Anthropic’s formalizes the Alpöge–Furman paper (17 comparator statements; “All Lean code was written by Claude”; review “author-verified”). Axiom’s formalizes Lamzouri’s proof (12 statements; certificates by AxiomProver per Lamzouri’s appendix; its “locally verified with the comparator” sentence dates from September 8, and its CI does not run the comparator; conditional on two inputs until October 3, now depending on Axiom’s fork of PrimeNumberTheoremAnd). Both report the comparator. Not built or run by us

Last checked October 27, 2026. Where it stands. Alpöge and Furman’s preprint is from August 13, revised on the 19th; Lamzouri’s is from September 2, revised on the 8th. Neither preprint has been published in a journal; Anthropic’s repository metadata says journal peer review is pending. No independent expert review is named in our sources. The paper says the proof was verified by Alpöge and Furman, the listed authors, who are mathematicians at Anthropic; the appendix says they read it in detail and condensed it to its present form. The paper thanks Brian Conrey and Daniel Goldston for reading the manuscript. Lamzouri’s paper is a second proof, by a different route, from a mathematician at the University of Lorraine. Anthropic’s Lean repository formalizes Claude’s paper; its metadata says Claude wrote all the Lean, Eric Easley orchestrated, and Ralph Furman checked the statements against the paper. Axiom’s repository formalizes Lamzouri’s proof; his appendix says AxiomProver generated the September version of those Lean certificates autonomously. Both say they pass the comparator. We did not build or run either.

The caveats. Lamzouri’s appendix describes Axiom’s certificate for the main theorem as resting on two assumed inputs; Axiom removed them on October 3, and the proof now depends on Axiom’s temporary fork of the PrimeNumberTheoremAnd project. The sources state the previous record differently: 40.75% in Lamzouri’s paper, five twelfths in Claude’s, and 41.6% in Anthropic’s post. If it holds, more than two thirds of the zeros of the Riemann zeta function are simple and on the critical line, unconditionally: found first by Claude, checked by its two authors at Anthropic, proved again by Lamzouri, and formalized in Lean. The Riemann hypothesis remains open.

Also in the sources: Anthropic’s 95-page account of how the argument was found says that its mathematics “has not been independently verified”, a caveat that “concerns this volume only, not the accompanying paper”. Lamzouri’s appendix describes Axiom’s certificate as it stood on September 8, before the October 3 change.

How the proof goes

  1. The question. Here is the history as Youness Lamzouri’s paper cites it. Hardy proved in 1914 that infinitely many zeros lie on the line, and Selberg in 1942 that a positive proportion do. Levinson got more than one third, and Conrey, in 1989, more than two fifths that are simple and on the line. In 2020, Pratt, Robles, Zaharescu and Zeindler reached 40.75%. A second line of work assumed the Riemann hypothesis. Montgomery used the pair correlation of zeros to show that at least two thirds would then be simple, and Montgomery and Taylor raised that to 67.25%. Recently Aryan proved an unconditional pair correlation formula for one kernel, and then Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh, made Montgomery’s pair correlation theorem work without the hypothesis.
  2. Claude’s route. How the proof goes, in Claude’s paper. Weil’s explicit formula pairs test functions through the zeros; the Riemann hypothesis is equivalent to that pairing being positive. The paper restricts it to a family of test functions spaced along the strip, about as many as there are zeros, and gets a large symmetric matrix. Each zero on the line adds a positive piece of rank one. Each pair of zeros off the line adds a block with one positive and one negative direction. Two quantities are computed: the trace, close to the number of zeros, and the sum of the squared entries, through Montgomery’s second moment, in the unconditional form of Aryan and of Baluyot and coauthors. A rank–trace inequality, which the paper calls the matrix form of m² ≥ 2m − 1, turns them into a lower bound: 2 − 4/3, or two thirds, with a flat window.
  3. Lamzouri’s route. Lamzouri’s route drops the matrix. He proves one Hilbert space inequality for any finite set of points that is symmetric under complex conjugation: the number of simple real points is at least twice the total, minus a double sum of a squared kernel. The rescaled zeros form such a set, and the double sum is again a pair correlation sum. He notes that both proofs lead to the same extremal problem of Montgomery and Taylor, which is why the constants agree.
  4. How it was found. How it was found, in Anthropic’s account. Jarred Sumner, an Anthropic staff member and not a mathematician, asked Claude to take a real stab at the Riemann hypothesis. At first, the post says, Claude generated and tried 650 ideas, none of which worked. Asked to try again, it coordinated about 60 Claude subagents, which ran 2,400 shell commands; the two sessions used 31 million output tokens. The post says Sumner’s input was mostly encouragement, such as keep going; the paper’s first page says he posed the problem and guided the investigation. The paper’s appendix says the argument first gave one half, then two thirds, and its acknowledgments call Sumner in every meaningful sense the paper’s human co-author.

The numbers in the video

  • Ours: the constants agree across the three sources’ formulas: C₀ = 3/2 − (1/√2)·cot(1/√2) = 0.6725007037, C₁ = (C₀ + 1)/2 = 0.8362503518, C₂ = 0.8876200082; every threshold quoted (67.25%, 83.62%, 88.76%) is below its constant.
  • Ours: the first 30 zeros of the zeta function (mpmath) all have real part 1/2, at heights 14.13, 21.02, 25.01, …, and each is simple (an illustration, not a proof).
  • Ours: a text scan of each Lean proof’s import closure (Mathlib excluded): Anthropic’s 190 files, Axiom’s 178 files (85 from the PrimeNumberTheoremAnd fork); no sorry. We did not build or run either.
  • From the sources: the flat window gives 2 − 4/3 = 2/3 (Claude’s paper); 650 ideas, about 60 subagents, 2,400 shell commands and 31 million output tokens (Anthropic’s post); the previous record stated as 0.407511 (Lamzouri), 5/12 (Claude’s paper) and 41.6% (Anthropic’s post, for zeros on the line).

Read the source

AI Proved What? is independent and not affiliated with Anthropic beyond using its product Claude, and not affiliated with Axiom.

Transcript

Read the full script

0:00The question

This is AN02. Before we start: AI Proved What? is made with Claude, Anthropic’s AI. This is Anthropic’s own result: we hold it to the same standards as every other lab’s, using only public sources. The Riemann zeta function has infinitely many zeros in a vertical strip, between real parts 0 and 1. The Riemann hypothesis says they all lie on the middle line, real part 1/2. Our script computes the first 30, which are known to lie on the line, at heights 14.13, 21.02, 25.01, and up. That is an illustration, not a proof. A zero is simple if it has multiplicity one, the way x vanishes at 0; x² has a double zero. The question: what share of all the zeros can be proved to be both simple and on the line? Here is the history as Youness Lamzouri’s paper cites it. Hardy proved in 1914 that infinitely many zeros lie on the line, and Selberg in 1942 that a positive proportion do. Levinson got more than one third, and Conrey, in 1989, more than two fifths that are simple and on the line. In 2020, Pratt, Robles, Zaharescu and Zeindler reached 40.75%. A second line of work assumed the Riemann hypothesis. Montgomery used the pair correlation of zeros to show that at least two thirds would then be simple, and Montgomery and Taylor raised that to 67.25%. Recently Aryan proved an unconditional pair correlation formula for one kernel, and then Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh, made Montgomery’s pair correlation theorem work without the hypothesis.

1:42The claim

Episode AN02 covers a result in three public documents. On August 10, 2026, Anthropic posted that an unreleased research version of Claude had improved a lower bound for the share of zeros on the line. On August 13, a preprint followed on arXiv, listing Levent Alpöge and Ralph Furman as authors. Its first page says: the mathematical argument in this paper was discovered and written by Claude, an AI developed by Anthropic. The listed authors verified the proof and take responsibility for its content. The theorem: unconditionally, as the height grows, at least two thirds of the zeros, counted with multiplicity, are simple and on the line, and at least five sixths are distinct. With Montgomery and Taylor’s window, the constants become 67.25% and 83.62%; the first is the number Montgomery and Taylor had reached assuming the Riemann hypothesis. The third document is Lamzouri’s. On September 2, Youness Lamzouri, of the University of Lorraine, posted what he calls a new, conceptually simpler proof of the same two bounds. A revision on September 8 added two estimates of his own: at least 88.76% of the zeros are simple or on the line. His abstract says the first proof was produced by an internal research version of Claude developed by Anthropic and subsequently verified by two mathematicians at Anthropic, Levent Alpöge and Ralph Furman, and that his additional estimates are neither stated nor proved in the Claude paper. He calls it a breakthrough result, and says the argument produced by Claude is technically intricate, and its main mechanism is not immediately transparent. What is not claimed. Not the Riemann hypothesis: Claude’s paper says the remaining third of the zeros are not shown to be off the line, merely not reached. Not that every zero is simple. These are limits as the height grows, not statements about any one zero. Anthropic’s post says: we don’t expect that the techniques Claude used will lead to proving the Riemann hypothesis. The paper says the Riemann hypothesis itself is out of reach of the mechanism, and puts the ceiling for certificates of this type near 68.2%, a bound worked out by Eric Easley and Stephen McAleer.

4:03How the proof goes

How the proof goes, in Claude’s paper. Weil’s explicit formula pairs test functions through the zeros; the Riemann hypothesis is equivalent to that pairing being positive. The paper restricts it to a family of test functions spaced along the strip, about as many as there are zeros, and gets a large symmetric matrix. Each zero on the line adds a positive piece of rank one. Each pair of zeros off the line adds a block with one positive and one negative direction. Two quantities are computed: the trace, close to the number of zeros, and the sum of the squared entries, through Montgomery’s second moment, in the unconditional form of Aryan and of Baluyot and coauthors. A rank–trace inequality, which the paper calls the matrix form of m² ≥ 2m − 1, turns them into a lower bound: 2 − 4/3, or two thirds, with a flat window. Lamzouri’s route drops the matrix. He proves one Hilbert space inequality for any finite set of points that is symmetric under complex conjugation: the number of simple real points is at least twice the total, minus a double sum of a squared kernel. The rescaled zeros form such a set, and the double sum is again a pair correlation sum. He notes that both proofs lead to the same extremal problem of Montgomery and Taylor, which is why the constants agree. How it was found, in Anthropic’s account. Jarred Sumner, an Anthropic staff member and not a mathematician, asked Claude to take a real stab at the Riemann hypothesis. At first, the post says, Claude generated and tried 650 ideas, none of which worked. Asked to try again, it coordinated about 60 Claude subagents, which ran 2,400 shell commands; the two sessions used 31 million output tokens. The post says Sumner’s input was mostly encouragement, such as keep going; the paper’s first page says he posed the problem and guided the investigation. The paper’s appendix says the argument first gave one half, then two thirds, and its acknowledgments call Sumner in every meaningful sense the paper’s human co-author.

6:11Where it stands

Where it stands. Alpöge and Furman’s preprint is from August 13, revised on the 19th; Lamzouri’s is from September 2, revised on the 8th. Neither preprint has been published in a journal; Anthropic’s repository metadata says journal peer review is pending. No independent expert review is named in our sources. The paper says the proof was verified by Alpöge and Furman, the listed authors, who are mathematicians at Anthropic; the appendix says they read it in detail and condensed it to its present form. The paper thanks Brian Conrey and Daniel Goldston for reading the manuscript. Lamzouri’s paper is a second proof, by a different route, from a mathematician at the University of Lorraine. Anthropic’s Lean repository formalizes Claude’s paper; its metadata says Claude wrote all the Lean, Eric Easley orchestrated, and Ralph Furman checked the statements against the paper. Axiom’s repository formalizes Lamzouri’s proof; his appendix says AxiomProver generated the September version of those Lean certificates autonomously. Both say they pass the comparator. We did not build or run either. The caveats. Lamzouri’s appendix describes Axiom’s certificate for the main theorem as resting on two assumed inputs; Axiom removed them on October 3, and the proof now depends on Axiom’s temporary fork of the PrimeNumberTheoremAnd project. The sources state the previous record differently: 40.75% in Lamzouri’s paper, five twelfths in Claude’s, and 41.6% in Anthropic’s post. If it holds, more than two thirds of the zeros of the Riemann zeta function are simple and on the critical line, unconditionally: found first by Claude, checked by its two authors at Anthropic, proved again by Lamzouri, and formalized in Lean. The Riemann hypothesis remains open.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.