Terence Tao - The integrated explicit analytic number theory network - IPAM at UCLA

Summary
Mathematician Terence Tao presents a progress report at IPAM (UCLA) on the Integrated Explicit Analytic Number Theory Network (IEANTN), an initiative launched in January 2026 to organize interdependent results in explicit analytic number theory into a “living spreadsheet” in Lean. Tao describes how the surge of AI-generated proofs and auto-formalization during summer 2026 initially led to bloated, unmaintainable formal code, prompting a major architectural pivot from a lemma-level graph to a node-based repository separating human-readable claims (Conclusions.lean), metadata (formalization.yaml), and AI-generated proof scripts (Solutions.lean) verified via the Lean Comparator.

---

What is shown

• [00:40] Slide Mathematics at scale: Tao explains the limitation of treating individual papers as the primary unit of mathematical output and proposes building multi-paper formal superstructures.
• [02:43] Slide What is explicit analytic number theory?: Explaining asymptotic bounds versus explicit error terms, detailing the Chebyshev $\theta(x)$ and $\psi(x)$ functions, Vinogradov’s three-primes theorem, and Helfgott’s 2013 proof of the ternary Goldbach conjecture.
• [07:06] Slide Explicit prime number theorem: Examining numerical tables and explicit bounds from Fiori–Kadiri–Swidinsky (2022) across different ranges of $x$.
• [09:00] Slide outlining the explicit number theory pipeline: from Riemann zeta zero-free regions (e.g., Mossinghoff–Trudgian 2015), to primary explicit estimates, secondary estimates, and applications like highly abundant numbers ($LCM(1, \dots, n)$ from a 2025 MathOverflow problem).
• [17:21] Slide The Integrated Explicit Analytic Number Theory Network: Outlining Phase 1 (formalizing literature into a Lean repository) and Phase 2 (AI tools auto-propagating constant updates).
• [20:13] Slide showing contributor statistics and subprojects upstreamed or submitted to Mathlib between January and June 2026.
• [21:32] Slide Jun–Aug: Explaining the breakdown caused by rapid auto-formalization tools (bloated AI proofs, redundant lemmas, and build times exceeding an hour).
• [24:50] Slide explaining the redesigned node architecture: Conclusions.lean (human-readable theorem statements), formalization.yaml (dependency and source metadata), and Solutions.lean (large AI-generated proof code verified once by Lean Comparator).
• [29:07] Network visualization graph showing paper/result nodes (color-coded by formalization status: statements in blue, verified in green, computational in yellow) and their directed dependency edges.

---

Claims & numbers

• Tao notes the IEANTN project was launched in January 2026 within the existing Prime Number Theorem and more (PNT+) formalization repository (presented at 17:21).
• By mid-2026, AI-generated formal proofs rapidly filled pending lemmas, but building the entire repository took more than an hour due to bloated, un-refactored formal code (presented at 21:32).
• Under the revised architecture, Conclusions.lean files are kept under ~500 lines for human auditability, while Solutions.lean files can reach 100,000+ lines of AI-generated proof code verified asynchronously by the Comparator in roughly 10–20 minutes (presented at 25:08, 27:26).
• With heavy AI solutions decoupled from the core library, the core Lean repository builds in approximately 10 minutes (presented at 27:50).
• Tao emphasizes that modern AI models allow converting static paper estimates into parameterized “pipeline” nodes that can propagate updated bounds automatically across mathematical dependencies (presented at 31:12).

---

Notable quotes

• [01:59] “The vision is to combine a large number of papers in this area into a single living ‘spreadsheet’, formalized in Lean.”
• [17:08] “This makes for an opportunity to deploy larger amounts of AI assistance than would otherwise be advisable for a mathematical project.”
• [23:02] “The codebase became a complete mess... building the entire project now took more than an hour, and the code was no longer human readable.”

---

Assessment
This is an authentic, official academic talk delivered by Terence Tao at an IPAM workshop at UCLA on September 17, 2026. Tao candidly details both successes and practical engineering bottlenecks in combining community formalization with high-throughput AI auto-formalization tools.

Described by gemini-3.8-flash on 2026-10-18 from the video’s audio and frames.