著名数学家陶哲轩（Terry Tao）近年来成为数学领域中人工智慧与电脑辅助证明（如 Lean4）的积极推动者。他从小便展现出非凡的数学天赋，曾是国际数学奥林匹亚最年轻的金牌得主，并于2006年获得菲尔兹奖。陶哲轩一向热衷于合作研究，并曾参与「博学计划」（Polymath Project）等大规模的群众外包数学合作，这奠定了他寻求以电脑自动化验证来解决大规模协同合作中错误检查瓶颈的理念。
在2023年，陶哲轩开始尝试并学习使用 Lean4 交互式证明系统，并成功将他与合作伙伴共同证明的「多项式 Freiman-Ruzsa (PFR) 猜想」进行了形式化。这次成功的合作经验证实了数学家可以在不需要深厚程式设计技巧的情况下，借由模组化拆解步骤，带领众多志愿者共同完成复杂证明的电脑验证。这项计划的效率预示了快速形式化数学证明的新时代。
随后，陶哲轩发起了名为「等式理论」（Equational Theories）的更大规模计划，旨在绘制数千个代数定律之间逻辑推导关系的完整地图。该计划在短短几天内便借由 Python 脚本、自动定理证明器以及人类数学家的协作，解决了数百万个推导关系，甚至在过程中发现了全新的数学结构。这项实验性数学的成功实践，展现出结合人类直觉、大语言模型与形式验证系统的全新数学研究范式。
Renowned mathematician Terry Tao has recently become a leading advocate for artificial intelligence and computer-assisted proofs, such as Lean4, in the field of mathematics. Exhibiting extraordinary mathematical talent from an early age, Tao was the youngest gold medalist in the International Mathematical Olympiad and won the Fields Medal in 2006. He has always favored collaborative research and participated in large-scale crowd-sourced math collaborations like the Polymath Project, which laid the foundation for his vision of using computer verification to overcome the bottleneck of manual error-checking.
In 2023, Tao began learning and utilizing the Lean4 interactive proof system, successfully formalizing the proof of the polynomial Freiman-Ruzsa (PFR) conjecture that he had solved with his collaborators. This successful effort demonstrated that mathematicians can lead formalization projects by modularizing proofs without needing advanced programming skills, relying instead on a network of volunteers. The project's remarkable efficiency heralded a new era of rapid formalization in mathematical research.
Following this success, Tao launched a larger project called "Equational Theories," aiming to map the logical implications among thousands of algebraic laws. By combining Python scripts, automated theorem provers, and human ingenuity, the decentralized team resolved millions of implications within days and discovered entirely new mathematical structures. This successful pilot project showcased a new paradigm of experimental mathematics that blends human insight, large language models, and formal verification systems.