IEEE Spectrum's latest feature on the future of AI in mathematics centers on Terence Tao's "Big Mathematics" proposal: an LLM-reasoning plus formal-verification workflow that rebuilds the trust mechanism for mathematical collaboration.
The core idea: today's mathematical collaboration depends on peer review and informal verification, both of which are bottlenecked by human bandwidth. Tao's proposal pushes the workflow into a "LLM proposes, formal system verifies" model — let the LLM do the heavy lifting of exploration and conjecture generation, and use proof assistants (Lean, Coq, Isabelle) to do the formal verification. The "trust" no longer relies on a reviewer's reputation, but on a mechanically checkable proof.
The technical path is becoming feasible: the latest LLM has demonstrated meaningful capability on formal-math tasks (e.g., AlphaProof at the IMO level), and proof assistants are becoming increasingly automated. Tao estimates that within 5-10 years, a "Big Mathematics" project of unprecedented scale — a million theorems with full formal verification — could become reality.
The bigger impact: this is not just a math-revolution story. The "LLM proposes + formal verification" pattern is generalizable to any "high-trust, high-cost" field — chip verification, contract audit, scientific paper review. Tao's experiment is, in essence, the first stress test of "AI-formal hybrid collaboration" at the frontier of human knowledge.
For the industry, the takeaway is that formal verification is moving from a "specialist tool" to a "general infrastructure." Whoever can lower the threshold of formal-verification use will reshape the next generation of research and engineering collaboration.