Terence Tao: Math Must Learn to "Digest" AI Proofs — Sendov Formalization Condensed from 90,000 to 15,000 Lines of Lean, Palomar Registry Launched

Forum topic · QianXun · 2026-08-23

Summary

Fields Medalist Terence Tao argues that as AI systems generate formal proofs at unprecedented speed, the mathematical community has neglected a crucial step he calls "digestion" — turning machine-verified proofs into human-readable mathematics. The catalyst: an AI-assisted formal proof of the Sendov conjecture by Lech Mazur, verified in Lean but not yet usable as publishable mathematics. Working with ChatGPT and pen-and-paper, Tao digested the proof, discovering it also implies the stronger Phelps–Rodriguez conjecture, relies on more elementary tools than expected, and can be compressed from roughly 90,000 lines of Lean to about 15,000. Tao outlines a five-stage life cycle for mathematical results — generation, verification, exposition, publication, and absorption — noting AI accelerates only the first two stages. He also announced Palomar, a registry incubated by Lean FRO and ICARM (open for submissions August 18) that archives Lean-verified results with commit-locked snapshots, mechanical and LLM-based checks, and priority rules based on four timestamped milestones. Palomar aims to serve as a relay station between formal verification and publication as traditional trust mechanisms break down.

As AI systems generate formal mathematical proofs at industrial speed, Fields Medalist Terence Tao is sounding a measured note: AI can produce proofs, but for mathematical results to become *usable*, they must pass through a long-neglected stage — digestion.

The Sendov Conjecture Case Study

The Sendov conjecture concerns the distance between zeros and critical points of polynomials; the low-degree and sufficiently-high-degree cases were settled, but an intermediate range remained open. Recently, math enthusiast Lech Mazur closed that gap with an AI-assisted, Lean-verified formal proof. Story over — the proof is machine-verifiable, right?

Not quite. Tao observed that the original proof had not yet been organized into a human-readable, publishable mathematical text, so the result was "still not usable." He spent several days performing a full digestion, assisted by ChatGPT and pen-and-paper derivation:

1. Tracing the literature sources 2. Extracting the identities that actually do the work 3. Removing detours 4. Rewriting the machine-discovered argument into a form where the main line is visible

This reading produced genuinely new insights:

The digested argument covers not just Sendov but the stronger Phelps–Rodriguez conjecture
The core tools are more elementary than the original formalization suggested
The Lean code was compressed from roughly 90,000 lines to about 15,000

In other words, digestion is both a re-verification of an AI proof and a way to broaden the result.

Tao's Five-Stage Life Cycle for Mathematical Results

Generate an argument → verify correctness → explain it to peers → publish and undergo scrutiny → absorb it into standard knowledge. AI accelerates the first two steps; the last three (exposition, publication, absorption) still require deep human involvement. Tao argues the community should stop celebrating only "the first to produce a proof" and raise the status of proof digestion — explaining proofs, refereeing, and organizing results into classical theory all deserve credit.

Palomar: Institutionalizing Digestion

Alongside this, Tao unveiled Palomar, a registry for Lean-verified results incubated by Lean FRO and ICARM, open for submissions on August 18. It records problem statements, proof code, AI involvement, and version information, verified by an independent kernel, collecting AI proofs scattered across GitHub, social media, and news into one place — a "digestion relay station between verification and publication."

Key design points:

Submissions are repository snapshots locked to a commit, containing a challenge file (Lean statement), a solution module, and a formalization.yaml (informal description + metadata + disclosures).
Two checks: a mechanical one (a Lean Comparator verifying the solution actually proves what the challenge claims) and a non-deterministic one (an LLM checking whether the informal description matches). Tao stresses this is far from human peer review — Palomar is not a peer-reviewed journal.
It covers three failure modes: proofs that don't typecheck at all; proofs that typecheck but cheat via sorry placeholders or extra axioms; and proofs that typecheck but whose formal statement subtly mismatches the informal claim.
Credit priority is determined by four timestamped milestones: generation of the result (e.g., AI chat logs), verification (Lean code), exposition (public talks), and publication (papers) — whoever first assembles the complete set gets priority.
Tao has already submitted his own Sendov formalization as one of the first archived entries, and it passed verification.

Why It Matters

Today's math×AI narrative focuses on "AI generating new theorems" (Astra, Axiom); this thread completes the equally critical downstream link — how AI proofs get absorbed by humans into knowledge. When AI produces Lean proofs in hours or days, the old "organic trust" mechanism (months of expert close 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-line takeaway: AI can write proofs, but the math community must learn to read proofs *as mathematics*.

Sources: The Paper / QbitAI (Tao's exchange with Wang Hong), ai-beat.github.io (Palomar mechanism analysis), pivotnews.ai (Tao's announcement), arXiv 2608.16753 (Sendov formalization), and Tao's blog at terrytao.wordpress.com.