Terence Tao on proof checkers and AI programs
AI-assisted proof systems such as Lean are beginning to change how advanced mathematics is done, prompting debate over whether they will soon become practical co-pilots for mainstream research or remain niche, labor-intensive tools. Commenters weigh the promise of automated theorem proving, neural-network-guided search and formal verification against current limitations in usability, data, and alignment with human mathematical intuition, and they question how careers, pedagogy, and even the nature of mathematical collaboration might shift. Underlying the exchange is a broader question of whether AI will merely mechanize tedious proof steps or eventually contribute genuinely new ideas and insights.
Role of AI in Mathematics
- Many see AI as a promising assistant for formal proofs, lemma search, and tedious case work, analogous to neural nets in chess engines rather than full automation of mathematics.
- Some expect AI will soon autocomplete or significantly assist in current research, though “math being solved in 2–3 years” is widely viewed as unrealistic.
- Others stress that even ugly, AI-found proofs are valuable starting points that humans can later simplify and understand.
Proof Assistants and Lean
- Proof assistants (Lean, Coq, Isabelle, HOL, Metamath, etc.) are central to the discussion; Lean is described as currently dominant in pure math, with a large library and strong community support.
- Tools like Isabelle’s Sledgehammer and Coq’s analogs already combine ATP/SMT solvers with interactive proof, though resulting proofs can be unreadable or brittle.
- Formalization is viewed as hard but increasingly feasible; some fields (logic, algebra) fit better than highly geometric or pictorial areas, though there are projects formalizing deep topology (e.g., sphere eversion).
Correctness, Complexity, and NP
- Multiple comments stress the distinction between finding a proof and checking one.
- Verification in typical proof systems is said to be linear in proof size: check axioms and each inference rule.
- There’s debate over complexity-theoretic framing (NP, k-SAT), but consensus that checking is much easier than search.
LLMs, Reliability, and “Hallucinations”
- Some worry that using LLMs to translate informal math to Lean could misrepresent the intended theorem; others reply that humans only need to verify the formal statement and definitions, since the checker guarantees the proof.
- A counterpoint notes that once AI also generates definitions, verifying they match intended concepts becomes nontrivial.
- Concrete anecdotes describe GPT-4 producing correct, useful lemmas and slick derivations, but also examples where it outputs superficially plausible yet incoherent or subtly wrong arguments.
Adoption and Career Dynamics
- One camp sees proof assistants as still niche and too costly for early-career researchers under publish-or-perish pressure; another reports active use, community growth, and even grants specifically for formalization.
- There’s discussion of emerging roles like “mathematical programmers” who formalize others’ proofs, reflecting a division of labor.
Broader Reflections
- Some compare the coming “project-managed” math ecosystem to the industrialization of software: less romantic individual genius, more coordinated large-scale projects.
- Opinions diverge on whether AI and mechanization herald a revolution in what math can tackle or a threat to the traditional culture of mathematics.