陶哲轩（Terry Tao）是世界著名的数学家，他自幼展现出惊人的天赋，10岁时便成为国际数学奥林匹克竞赛最年轻的奖牌获得者，并在24岁时获得加州大学洛杉矶分校的终身教职。2006年，他因在数论领域的杰出贡献荣获菲尔兹奖。尽管他具备独自工作的能力，但陶哲轩一直推崇合作，认为集体智慧是推动数学发现的关键。他曾通过博客等公开平台倡导大规模协作，并在2009年参与了蒂莫西·高尔斯（Timothy Gowers）发起的“Polymath计划”，尝试以群体众包的方式解决复杂的数学难题。
随着对计算机辅助验证数学证明兴趣的日益浓厚，陶哲轩开始关注交互式定理证明系统Lean。他意识到，大规模的人类协作往往受限于错误检查的瓶颈，而机器验证能够提供一种高效的自动化方案。2023年，在正式学习Lean之后，他领导了“多项式弗雷曼-鲁扎（PFR）猜想”的正式化工作。通过将复杂的数学证明拆解为多个微小的引理，他成功动员数十名志愿者在短时间内完成了证明的正式化，这不仅验证了该领域的重要性，也展示了人类洞察力与人工智能辅助工具结合的巨大潜力。
进入2024年，陶哲轩在担任拜登总统科学技术咨询委员会成员期间，进一步推动了数学研究范式的转变。他发起了“等式理论（Equational Theories）”项目，旨在通过大规模自动化搜索和群体协作，绘制4694种代数定律之间2200万个逻辑蕴含关系的完整蓝图。尽管该项目引发了部分学者的质疑，但它确实揭示了如“岩浆上同调（magma cohomology）”等全新的数学概念。陶哲轩认为，数学正处于向“实验性科学”演进的关键节点，未来数学家将能够利用大语言模型和形式化验证系统，以类似于物理学大规模协作的方式，探索数学知识的未知前沿。
Terry Tao, a Fields Medalist and globally recognized mathematician, has long championed unconventional methods and collaborative research. Born in 1975, he exhibited prodigious talent early, becoming the youngest person to win a gold medal at the International Math Olympiad at age 10. Despite his ability to work independently, Tao views collaboration as a catalyst for innovation. He was a central figure in the 2009 Polymath Project, an initiative designed to solve major problems through mass, open-source mathematical cooperation.
Recognizing the limitations of human-only moderation in large-scale projects, Tao turned his attention to formal verification systems like Lean. In 2023, he led an effort to formalize the polynomial Freiman-Ruzsa (PFR) conjecture. By decomposing the proof into modular segments, he successfully mobilized a community of volunteers to verify the result using Lean. This experiment served as a proof of concept, demonstrating that formalization could be decentralized and accelerated, effectively bypassing traditional, bottleneck-heavy verification processes.
By 2024, as a member of President Joe Biden’s Council of Advisors on Science and Technology, Tao intensified his advocacy for machine-assisted mathematics. He launched the Equational Theories project, a massive effort to map 22 million logical relationships between 4,694 algebraic laws. The project utilized automated theorem provers and human contributions to resolve nearly all implications, leading to the discovery of novel concepts like magma cohomology. Tao believes that mathematics is evolving into an experimental discipline, where human insight, AI, and formal verification combine to transform how new truths are uncovered, moving the field toward a future of large-scale, automated scientific exploration.