Terence Tao on proof checkers and AI programs

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.