Claude has improved on a longstanding lower bound for the fraction of zeros of the Riemann zeta function that satisfy the Riemann hypothesis

A new proof that more than $2/3$ of the zeros of the Riemann zeta function are simple and on the critical linearXiv.orgYouness LamzouriSep 2, 2026in the index

We obtain a new, conceptually simpler, unconditional proof that more than $67.25\%$ of the non-trivial zeros of the Riemann zeta function are simple and on the critical line, and that at least $83.62\%$ of the non-trivial zeros are distinct. Our approach also yields two new unconditional estimates…

Reliability of Anthropic's Lean verificationsmathoverflow.netHenri CohenOct 20, 2026

This morning appeared on arXiv a very nice paper by Arias de Reyna entitled "Human exposition of Claude's 2/3 theorem on the zeros of zeta" which does exactly what the title says (I am eagerly waiting for a similar paper for quasi-RH). I was struck by the following paragraph: "As it's written, [1]…

Answer to: Reliability of Anthropic's Lean verificationsmathoverflow.netTimothy ChowOct 20, 2026

Without looking at the details of this specific case, I can describe the typical scenario. A "flagship theorem" is (allegedly) proved (by AI models, let's say). Some natural-language proof is produced. The statement of the flagship theorem is formalized in Lean. A Lean proof of the formalized…