The Mathocalypse
AI-generated proofs of hundreds of long‑standing math problems are prompting both awe and alarm among researchers. Commenters weigh the significance of Lean-verified but often unreadable proofs, raising concerns about mistranslation from natural language, possible errors, loss of human-understandable insight, and the impact on careers, incentives, and academic culture. Many see an inevitable shift toward using AI as a core tool in mathematical research, but strongly disagree over trust in the companies involved and how (or whether) human mathematicians will retain a meaningful role.
Nature of the AI results
- Many see the work as “statistically guided brute forcing” that yields correct answers but little understanding; others argue that’s still genuine progress, like evolution’s brute-force search producing biology.
- Breaking long-standing complexity barriers (e.g., shaving exponents slightly) is defended as important because it disproves optimality conjectures, even if the improvement looks numerically tiny.
- Some commenters emphasize that solving ~5% of ~8,000 hard problems after a few hours of compute each is astonishingly strong and economically cheap per result.
Legibility and verification
- Multiple reports say many papers are badly written, opaque, and feel like “psychedelic” or “messy code” math: logically dense, poor exposition, heavy name-dropping, unclear use of prior work.
- Lean certificates are widely cited as evidence the formal statements are correct, but:
- Autoformalization can mistranslate natural-language proofs into Lean.
- A separate paper argues such translation is extremely hard in principle, and shows concrete mismatches (including for the Navier–Stokes result).
- Some raise the possibility of Lean bugs or exploit-like behavior, though others say known soundness bugs are esoteric.
- Precedent like the computer-assisted Four Color Theorem is invoked: correctness can be accepted even when human-comprehensible proofs are lacking, but many still want simpler proofs later.
Impact on mathematics and careers
- Strong anxiety from PhD students and young researchers: fear that skills and problems are being automated away, and that AI has created an uneven playing field (closed internal models scooping years of work).
- Others argue math was never mainly about collecting theorems; the real value is new concepts and machinery. Humans can:
- Distill and explain AI proofs.
- Extract new techniques.
- Decide which questions and ideas are interesting.
- Some think we will need more mathematicians to interpret, structure, and build on AI outputs; others expect funding and incentives to shift away from humans.
Trust, ownership, and incentives
- Deep distrust of closed labs: questions about provenance of proofs, possible appropriation of user ideas, and PR/IPO motivations.
- Suggestions: delay using internal models to scoop external researchers; share tools earlier; or treat “translation and explanation” as a new professional role deserving credit.
- Debate over whether it is acceptable to flood the field with hundreds of unreadable preprints; some defend open release over traditional peer review, others call it irresponsible “slop”.
Comparisons to coding and tooling
- Many liken this to gen-AI code: AI produces sprawling, hard-to-read “PRs” that technically work but require tedious human review.
- Similar concerns: lack of clean abstractions, difficulty building towers of understanding on messy artifacts, and a shift from creating to auditing.
Expectations about future AI progress
- Optimists assume models will soon also generate elegant, human-scale explanations; skeptics compare such confidence to past overhyped tech (crypto, full self-driving).
- Some argue that, as systems surpass human cognitive limits, fully human-legible proofs may become impossible in many cases, making layered verification and “observability tools” more important than direct comprehension.