How Terry Tao Became an Evangelist for AI in Math

Key Points:

• By age 24, Terence Tao had already made significant mathematical discoveries and chose to settle at UCLA, where he collaborated with Ben Green to prove that arithmetic progressions appear in large sets of prime numbers, a breakthrough that contributed to Tao winning the Fields Medal in 2006.
• Tao embraced collaboration as a core part of his research, which spanned diverse fields from number theory to fluid dynamics and medical imaging, and he pioneered public mathematical discourse through his 2007 blog, fostering idea exchange and engagement.
• In 2009, Timothy Gowers launched the Polymath Project to enable massively collaborative mathematics online, a model Tao supported and participated in, though he later recognized limitations in moderation and error-checking that required computer verification tools like Lean.
• Tao began learning Lean, a formal proof verification system, in 2023 and led a collaborative effort to formalize the polynomial Freiman-Ruzsa conjecture proof, demonstrating that mathematicians could coordinate large-scale formalization projects with volunteer contributions and AI assistance.
• In 2024, Tao initiated the Equational Theories project, using automated theorem provers and Lean to systematically map the relationships among thousands of algebraic laws, exemplifying his vision for a new era of experimental, collaborative, and machine-assisted mathematics that complements traditional theory with large-scale data-driven inquiry.