Terence Tao's ICM 2026 'Proof Indigestion' Warning and Anthropic's Claude Pushing the Riemann Zeta Zero Lower Bound to 67.2%

Forum topic · 小凯 · 2026-08-31

Summary

At ICM 2026, Terence Tao delivered a keynote titled 'Mathematics in the Age of AI,' diagnosing what he called a once-in-a-century crisis for mathematics. Citing First-Proof Project round-two results—where AI systems solved 7 of 10 novel research-level problems at $10–$1,000 per problem—Tao argued the field is shifting from 'proof scarcity' to 'proof surplus.' He outlined a five-gate pipeline (generation, verification, explanation, peer acceptance, canonization) in which AI has already automated the first two but left the last three to humans, coining 'proof indigestion' for the widening gap between one-hour machine proofs and days-long human digestion. Complementing this macro view, Anthropic reported in August 2026 that an unreleased Claude research model raised the unconditional lower bound on Riemann zeta zeros on the critical line from 41.6% to 67.2%—the first advance beyond Levinson's method since 1974—using ~60 sub-agents, 31M output tokens, 54 reviewed arXiv papers, and a fully formalized, sorry-free Lean 4 proof published on GitHub. Tao's proposed responses include the Leiden Declaration on AI disclosure and a rule that authors must be able to explain their results at an expert level before publishing. The post also contrasts this with OpenAI's 250k-line Lean proof of the 78-year-old Hopf conjecture and surveys open questions for the next 6–12 months.

Key points

Tao's ICM 2026 diagnosis: a 'century crisis' for mathematics

In July 2026, Terence Tao gave a public lecture at the International Congress of Mathematicians (ICM 2026) titled *Mathematics in the Age of AI*, framing today's situation as analogous to the 1900–1930 foundational crisis (Russell's paradox, Gödel incompleteness). This time, however, the crisis concerns the value and practice framework of mathematics: what counts as a contribution, what should be rewarded, what 'understanding' means, and whether a machine can be said to have 'completed' work.
Tao repeatedly cited the First-Proof Project round-two data: on May 28, 2026, 10 never-before-published research-level problems were given to 4 AI systems under controlled conditions. 7/10 problems were solved at publishable quality by at least one system, at a compute cost of $10–$1,000 per problem.

The five-gate pipeline and 'proof indigestion'

Tao decomposes mathematical problem-solving into five gates:

| Gate | Meaning | AI status | | --- | --- | --- | | 1. Proof generation | From 'open problem' to 'solved' | Done | | 2. Proof verification | Confirm logical correctness | Semi-automated (AI + Lean) | | 3. Proof explanation | Articulate the reasoning | Gap | | 4. Peer acceptance | Community willing to learn it | Gap | | 5. Canonization | Enter textbooks as common knowledge | Gap |

Tao's recurring example: when reading Bourgain's papers, his margins filled with completed steps, question marks, and rewritten proofs — 'understanding forms precisely in the process of getting stuck and rewriting.' AI-generated papers read smoothly and treat hard and routine steps with equal ease, hiding the cognitive map of 'where to slow down.'
In summer 2026, AI systems overturned four decades-old conjectures, including the Jacobian conjecture (87 years) and the Hopf/six-sphere problem (78 years). Yet Tao himself spent several days rewriting a proof the AI produced in one hour into a human-readable version. He named this worsening ratio 'proof indigestion.'

Anthropic's Claude Riemann zeta breakthrough: 41.6% → 67.2%

On August 10, 2026, Anthropic announced that an unreleased research build of Claude, asked to 'take a real stab at the Riemann hypothesis,' produced a new unconditional lower bound on zeta zeros on the critical line: 67.2%, up from 41.6% (Levinson-method lineage: 33.3% in 1974, ~41.7% in 2020).
This is the first escape from the Levinson method's ceiling since 1974: Claude combined Montgomery's 1973 pair-correlation method with Bombieri's 2000 work on Weil quadratic forms, using recent papers by Baluyot, Goldston, Suriajaya, and Turnage-Butterbaugh (2023–2025) to strip out RH-dependent conditions.
The same work also pushed the 'distinct zeros' record from Wu 2016's 66.03% to 83.6% — two records in one paper.

Anatomy of the run

| Dimension | Round 1 | Round 2 | | --- | --- | --- | | Form | Single agent, generate + verify | Multi-agent coordination | | Failed ideas | ~650 | 0 (all done in round 1) | | Output tokens | Small | 31M | | Sub-agents | – | ~60 | | Shell commands | – | ~2,400 | | Python scripts | – | Hundreds | | Numerical checks | – | Thousands | | arXiv papers reviewed | – | 54 |

The run spanned two Claude Code sessions, with three layers of human review (Anthropic in-house mathematicians Levent Alpöge and Ralph Furman, plus external experts Brian Conrey and Dan Goldston).
A public Lean 4 formalization was released at GitHub repo anthropics/zeta-23-lean. Theorems A through E were all formalized sorry-free, with no extra axioms beyond Lean's own three — the first mechanically verifiable complete proof at this depth produced in an AI + formalization collaboration.

Tao's proposed responses

1. Five-layer model: AI + programs handle generation and verification; humans lead on explanation, acceptance, and canonization. 2. Leiden Declaration on AI and Mathematics (June 2026), endorsed by Tao: disclose AI usage; de-emphasize 'who solved it first' and elevate 'digestion' (explanation, publication, canonization); humans remain accountable for correctness and attribution. 3. 'Demonstrate you can explain it' rule: > 'If the author cannot convincingly demonstrate they can give a clear, expert-level, correct, and properly attributed talk on the result, then the result should not be published.'

Even Lean-verified results should not be published under a human name if the author cannot explain them at an expert level. Critics invoke chess engines ('ground truth exceeds human explainability'); supporters counter that mathematics is fundamentally a human endeavor of understanding, with ground truth as a byproduct.

Relation to the Hopf conjecture breakthrough (Aug 28)

| Dimension | Hopf single-point proof | ICM 2026 systemic warning | | --- | --- | --- | | Focus | One specific conjecture proven by AI | Entire discipline's paradigm restructured | | Actor | Boris Alexeev, OpenAI, 250k-line Lean | Terence Tao, ICM keynote | | Stack | OpenAI + 250k lines Lean + 250k lines math | Anthropic Claude + 60 sub-agents + Lean |

The two are complementary: a micro-level formalization breakthrough plus a macro-level paradigm shift, together putting the question 'does mathematics still need human mathematicians?' formally on the table.

Emergent multi-step reasoning

Comparing Claude's Riemann run with Anthropic's cybersecurity runs (269 projects tested, 1,097 critical vulnerabilities found), the common thread is emergent multi-step chain reasoning arising from training targets aimed only at single-step capability. Any product treating AI as a 'single-step tool' will hit this wall.

Watch list for the next 6–12 months

1. Will the Claude zeta paper enter peer review (currently blog + Lean formalization only, not yet on arXiv)? 2. Can the 67.2% bound be independently reproduced, given the model is unreleased — the new 'auditable vs. reproducible' gap in AI for Science? 3. Diffusion of the Leiden Declaration (already IMU-endorsed); will 10+ top journals sign AI-disclosure statements by 2027 H1? 4. Practical enforcement of the 'demonstrate you can explain it' rule; possible emergence of 'AI proof explanation' as a job category. 5. First-Proof round 3: how far will pass rates drop as difficulty rises — potentially the 'trigger point' Tao says is needed for proof surplus to become consensus.

References

toolai.io: Terence Tao Warns of a New Century Crisis in Mathematics at Fields Medal Ceremony
Tech Times: Claude Raises Riemann Zeta Zeros to 67.2%: Two Papers No One Had Combined
AI Weekly: Anthropic says Claude improved a Riemann zeta lower bound
AI Bacon: 41.6% to 67.2%: Claude Broke a Riemann Record It Wasn't Chasing
Anthropic: Learning more about Claude's mathematical capabilities