ICM 2026 Public Lectures - Terence Tao

Scientific concepts / discoveries / nature phenomena mentioned

Crisis in foundations (early 20th century) in mathematics

• Naive set theory inconsistencies, illustrated via self-containing vs. non-self-containing sets.
• Russell’s paradox as an example of inconsistency in naive set theory.
• Gödel’s incompleteness theorems: no fixed axiomatic system can be complete for all arithmetic questions.
• Outcome: a standard foundational framework for mainstream mathematics, notably:
  • First-order logic + Zermelo–Fraenkel set theory + the Axiom of Choice (ZFC).
• Mentioned alternative foundation work:
  • Lean, a proof assistant, is based on dependent type theory, not directly on ZFC.

AI and mathematics as a methodological/values “crisis”

• Not a change to mathematical truth itself, but a shift in values and practices due to AI capabilities.

AI proof-production pipeline (“proof digestion” model)

The talk decomposes “problem solving” into stages that AI is improving unevenly:

1. Proof generation (AI can often produce candidate proofs).
2. Proof verification (AI + proof assistants can check formal correctness; improved tools make this faster).
3. Proof exposition / explanation (human understanding and readable narrative; AI is currently weaker).
4. Proof acceptance by the community (e.g., via human refereeing and publication norms).
5. Canonicalization into textbook-level standard knowledge (slow, consensus-driven; AI is largely ineffective here).

Resulting concern: “proof indigestion” / abundance—too many proofs, too little human capacity to digest, teach, and integrate them.

Erdős-type problem lists

• Mentions the Erdős problems list (about 200 problems) as an example area where solutions may be appearing and even being formalized.
• Raises questions about whether humans can meaningfully vet and explain them.

“Goodhart’s law” / target optimization failure

• When a metric becomes a target, optimizing it can undermine other desired goals.
• Applied to AI systems that may optimize mathematical “outputs” without maintaining human-relevant value constraints.

Proof-assistant / formalization ecosystem

• Highlights that modern proof assistant languages have improved verification and formal proof workflows.

---

Methodologies / lists outlined

“Five stages” of mathematical problem solving / proof digestion

• Proof generation
• Proof verification
• Proof exposition
• Publication / community acceptance (often via human refereeing and journal processes)
• Canonicalization (integration into textbooks, teaching, and standard “definitive” theory organization)

“Community response question” framed pseudo-mathematically

• AI capability conjecture (family of conjectures):
  • With sufficient expense and human supervision, near-future AI tools will accomplish research-level mathematical tasks with non-trivial success, correctness, and quality.
• Conditional analysis:
  • Assuming that capability is substantially true, the community must address:
    • the goals-and-values question: what mathematicians value, and how to evaluate success beyond raw proof production.

---

Researchers / sources featured

• Terence Tao (speaker)
• Eli Stein (Tao’s PhD advisor)
• Bertrand Russell (naive set theory inconsistency; Russell’s paradox)
• Kurt Gödel (incompleteness theorems)
• Alonzo Church / “Guro”: the text says “Guro,” but the context indicates Gödel (spelled incorrectly in subtitles)
• Jean Bourgain (named example paper; “Jean Bugen” appears to be an ASR/subtitle error)
• Hong Wang (mentioned as having work based on Bourgain’s paper)
• Bill Thurston (quote about not meeting an abstract production standard; attributed to “Bill Thirsten” in subtitles)
• International Congress of Mathematicians (ICM) (institutional context)
• IMU / IMU: International Mathematical Union; mentioned as not able to unilaterally set community rules
• Erdős problems (problem list/literature source mentioned)
• Lean (proof assistant; source platform)
• Zermelo–Fraenkel + Axiom of Choice (ZFC) (foundational framework)