Terence Tao: Math Should Learn to 'Digest' AI Proofs — Sendov Formalization Compressed from 90K to 15K Lines, Palomar Registry Launches

Forum topic · QianXun · 2026-08-23

Summary

Terence Tao argues that AI-generated mathematical proofs require a crucial but overlooked step he calls 'digestion' before they become usable mathematical knowledge. After AI-assisted work produced a Lean-verified proof of the Sendov conjecture's remaining cases, Tao spent days reconstructing the argument with ChatGPT and pencil-and-paper, distilling key identities and streamlining detours. The digested proof turned out to be stronger: it also covers the Phelps–Rodriguez conjecture, relies on more elementary tools than the formalization suggested, and shrunk the Lean code from roughly 90,000 to 15,000 lines. Tao proposes a five-stage lifecycle for results—generation, verification, exposition, publication, institutionalization—and calls on the community to credit proof digestion alongside discovery. He also announced Palomar, a registry incubated by Lean FRO and ICARM that archives Lean-verified results with commit-locked snapshots, mechanical and LLM-based checks, and timestamped priority attribution, serving as a relay station between verification and publication.

Terence Tao: Math Should Learn to 'Digest' AI Proofs

While AI systems generate Lean-verified proofs of open problems at increasing speed, Fields Medalist Terence Tao has raised a cooler-headed point in his ICM lecture and blog: AI can produce proofs, but for results to become *usable* mathematics, the community must perform a long-neglected step — digestion.

What 'digestion' means: the Sendov conjecture case

The Sendov conjecture concerns the distance between polynomial zeros and critical points; the low-degree and sufficiently-large-degree regimes were solved, leaving a gap in between. Recently, math enthusiast Lech Mazur used AI to fill this gap with a Lean-verified formal proof.

Tao observed that this raw proof had not yet been organized into a human-readable mathematical text — the result was "still not usable." He then spent several days performing a full digestion, assisted by ChatGPT and pencil-and-paper:

Tracing the literature sources
Extracting the identities that actually do the work
Removing detours
Rewriting the machine-discovered argument into a version with a visible main line

This digestion produced new findings: the cleaned-up argument not only settles Sendov but also covers the stronger Phelps–Rodriguez conjecture; the core tool is more elementary than the original formalization suggested; and the Lean code shrank from ~90,000 lines to ~15,000 lines. Digestion, in other words, is both re-verification of an AI proof and a path to broadening the result.

Tao's five-stage lifecycle of a mathematical result

1. Generate the argument 2. Verify correctness 3. Explain it to peers 4. Publish and face scrutiny 5. Settle into standard knowledge

AI accelerates the first two stages; the last three (exposition, publication, institutionalization) still demand deep human involvement. Tao argues the community should stop over-valuing "first to prove" and raise the status of those who digest, explain, review, and organize proofs into classical theory.

Palomar: institutionalizing digestion

Tao simultaneously unveiled Palomar, a registry for Lean-verified results incubated by Lean FRO and ICARM (open for submissions August 18). It registers problem statements, proof code, AI involvement, and version information, cross-checked by an independent kernel — a central collection point for AI proofs scattered across GitHub, social media, and news, acting as a "digestion relay between verification and publication."

Mechanism design highlights:

Submissions are repository snapshots locked by commit, containing a challenge file (Lean declarations), a solution module, and a formalization.yaml (informal description + metadata + disclosure).
Two checks: mechanical (a Lean Comparator verifies the solution proves what the challenge claims) and non-deterministic (an LLM checks the informal description matches). Tao stresses this is far from human peer review — Palomar is not a peer-reviewed journal.
Covers three failure modes: the proof doesn't typecheck; it typechecks but cheats (e.g., sorry placeholders or extra axioms); it typechecks but the formal statement subtly mismatches the informal claim.
Credit is determined by four timestamped milestones: generation (e.g., AI chat logs), verification (e.g., Lean code), exposition (e.g., public talks), and publication (e.g., papers) — whoever submits a complete set first gets priority.
Tao has already submitted his own Sendov formalization among the first archives, and it passed verification.

Why it matters

Today's math × AI narrative focuses on "AI generating new theorems" (Astra/Axiom), but this line completes the equally critical downstream question: how AI proofs get absorbed into human knowledge. When AI mass-produces Lean proofs in hours or days, the old "organic trust" mechanism (months of expert reading, author reputation) breaks down; Palomar is an attempt to replace it with automated audit trails. It doesn't care about provenance (human/AI/hybrid) — only correctness, which is precisely the pressure that created the need for a registry.

One sentence: AI can write proofs, but the math community must learn to read proofs as mathematics.

Sources: The Paper / QbitAI; ai-beat.github.io (Palomar mechanism analysis); pivotnews.ai (Tao's announcement); arXiv 2608.16753 (Sendov formalization); terrytao.wordpress.com.