生成式与推理式协同：陶哲轩论当代AI的数学能力边界与研究范式革新
日期：2026年2月23日
中文摘要
本文以菲尔兹奖得主陶哲轩关于人工智能与数学研究的系列演讲、实证工作及公开论述为核心依据，结合埃尔德什问题集的大规模AI实验数据，系统阐释陶哲轩对当代人工智能数学水平的界定与研判。研究指出，陶哲轩将AI划分为生成式概率型AI与推理式形式化AI两类互补工具，前者以大语言模型为代表，承担文献检索、思路生成、数值实验等任务，后者以Lean定理证明器为核心，承担严格逻辑验证与证明保真功能。通过对1300余道埃尔德什问题的AI求解实践表明，当前AI仅具备规模化处理中等难度、低关注度长尾问题的能力，尚不具备自主数学理解、原创理论构造与顶级数学难题攻坚能力。AI的真正价值在于推动数学研究从传统手工作坊式小团队攻关，向众包化、规模化、形式化新范式转型，实现人类原创洞察与机器高效运算的深度协同。本文同时澄清了“AI已达到专业数学家水平”等行业炒作，明确了人机协作在数学研究中的主导地位与未来路径。
关键词：陶哲轩；人工智能；数学研究；形式化验证；Lean；埃尔德什问题集；人机协同
English Abstract
Based on a series of lectures, empirical work and public discussions by Fields Medalist Terence Tao on artificial intelligence and mathematical research, combined with large-scale AI experimental data from the Erdős Problems, this paper systematically interprets Terence Tao’s definition and judgment on the mathematical ability of contemporary artificial intelligence. The study points out that Terence Tao divides AI into two complementary tools: generative probabilistic AI and reasoning formal AI. The former, represented by large language models, undertakes tasks such as literature retrieval, idea generation, and numerical experiments; the latter, with Lean theorem prover as the core, undertakes strict logical verification and proof fidelity functions.
The practice of solving more than 1,300 Erdős Problems by AI shows that current AI only has the ability to process medium-difficulty, low-attention long-tail problems on a large scale, and does not have the abilities of autonomous mathematical understanding, original theoretical construction, or tackling top mathematical problems. The real value of AI lies in promoting the transformation of mathematical research from the traditional manual workshop-style small-team tackling to a new paradigm of crowdsourcing, large-scale and formalization, realizing the deep collaboration between human original insights and efficient machine computing. This paper also clarifies the industry hype such as "AI has reached the level of professional mathematicians" and defines the dominant position and future path of human-machine collaboration in mathematical research.
Key words: Terence Tao; Artificial Intelligence; Mathematical Research; Formal Verification; Lean; Erdős Problems; Human-Machine Collaboration
一、引言
数学作为人类知识体系中最严谨的基础学科，长期保持着高度保守的研究范式。从柯西时代的复分析教材到当代课堂，核心内容与表述方式近200年未发生本质改变；黑板仍是主流研究工具；数学论文的合作人数远低于物理、化学、生物等实验学科，难以实现科研的规模化与产业化（陶哲轩，2026）。人工智能的快速崛起，正在为这一古老学科注入结构性变革动力。然而，科技行业对AI数学能力存在大量夸大宣传，部分机构宣称AI“已解决多项世界级难题”“达到数学家水平”，形成了认知偏差与泡沫化判断。
陶哲轩作为当代最具影响力的数学家之一，自2023年起持续以埃尔德什问题集为实验基准，开展AI与数学研究的大规模实证探索，并在UCLA IPAM研究所“AI for Science”论坛中系统提出了对AI真实水平的判断框架。他拒绝将AI神化或简单工具化，而是从数学研究的真实逻辑出发，将AI理解为生成式智能与推理式智能结合的协同系统，为理解AI的能力、边界与未来价值提供了顶级科学家的理性视角。
本文基于陶哲轩演讲原文、学术论文、社区记录及相关AI定理证明研究，完整还原其AI观，并以埃尔德什问题集为实证案例，揭示当代AI的真实数学水平，最终归纳AI驱动下数学研究范式的革新路径。
二、陶哲轩对AI的核心定义：两类智能的协同体
陶哲轩并未将AI视为具有意识、理解或自主思考能力的通用智能，而是从数学研究的实用性出发，将AI明确划分为两种功能完全不同、但必须配合使用的智能形态。
（一）生成式AI：概率型猜测与规模化处理工具
以Gemini、GPT系列、AlphaEvolve为代表的大模型，在陶哲轩的定义中属于生成式、概率型AI。其本质是基于海量文献与数据的模式匹配机器，不具备对数学定义、定理与结构的真正理解（Tao，2026）。它能够生成证明草稿、检索文献、构造数值案例、绘制数学图表，但存在固有的“幻觉”问题，会编造引理、篡改文献、伪造逻辑步骤。
生成式AI的核心价值在于突破人类注意力瓶颈：能够快速遍历上千道问题、批量尝试数十种解题技术、挖掘数十年前跨领域冷门文献，完成人类不愿做、没时间做、效率极低的重复性工作。
（二）推理式AI：形式化验证与逻辑保真工具
陶哲轩明确将Lean定理证明器及其自动化工具（如Aristotle、Lean Copilot）归入推理式AI的范畴。它不依赖概率生成，而是基于类型论与自动推理算法，对数学证明进行逐行、逐步骤的严格检查，确保证明100%逻辑正确（Song et al.，2025）。
Lean的出现，解决了生成式AI最致命的缺陷：不可靠性。陶哲轩多次强调：没有形式化验证的AI证明，都是不可信的；只有经过Lean编译通过的证明，才能进入数学知识体系。因此，Lean并非简单的软件，而是AI时代数学研究的逻辑基础设施。
（三）陶哲轩AI观的核心结论
AI = 生成式AI（大胆猜想） + 推理式AI（小心求证） + 人类数学家（方向与创新）
三者缺一不可，共同构成新一代数学研究模式。
三、AI数学能力的实证基准：埃尔德什问题集
为客观衡量AI水平，陶哲轩选择了埃尔德什问题集作为全球首个大规模数学AI测试基准。
（一）数据集背景
埃尔德什（Paul Erdős）是20世纪最多产的数学家，一生提出超过1500个数学问题。2023年，数学家托马斯·布鲁姆（Thomas Bloom）建立专门网站，系统整理收录1300余道问题，覆盖数论、组合、图论、几何、分析等领域，难度从初等问题到世界级开放难题（Bloom，2023–2026）。
（二）AI在问题集上的真实表现
截至2026年2月，1300余道问题中约480道已解决，699道未解决。陶哲轩通过数据得出关键结论：
AI解决的绝大多数是少人关注、文献稀少、难度中等的“长尾问题”；
AI几乎没有在数学界高度关注、悬赏高、需要原创思想的核心难题上取得突破；
AI的核心贡献是文献深度检索与证明形式化加速，而非独立创造新数学。
陶哲轩团队公开的两个典型案例均为人机协作：
问题367：爱好者提出思路→陶哲轩调用Gemini补全关键步骤→Lean完成验证；
问题1026：人类提出猜想→AI将问题转化为正方形填充问题→结合已有成果完全解决。
这印证了陶哲轩的判断：AI不独立解题，人机协同才解题。
（三）对行业炒作的澄清
陶哲轩直接反驳“AI达到数学家水平”的说法：数学研究的核心是理解、构造、推广与理论创新，而非单纯解题。AI只完成了最表层的任务，远未触及数学研究的本质。
四、AI推动的数学研究范式革新
陶哲轩认为，AI的真正意义不在于解出几道题，而在于彻底改变数学的生产方式。
（一）从手工作坊到规模化科研
传统数学难以规模化的三大障碍：门槛高、验证难、协作难。AI+Lean解决了这些问题：非专业人士（高中生、程序员）可参与；形式化验证自动保证正确性；跨国社区可实时协作。数学第一次具备了众包科研的可能。
（二）从个人灵感驱动到数据驱动
过去数学依赖天才灵感，未来数学将是小团队攻坚顶级问题 + AI大规模清扫长尾问题并行。埃尔德什问题集正是这一新模式的典范。
（三）从口头证明到形式化证明
AI推动数学进入形式化时代。未来的数学论文将以Lean代码为可信基础，彻底杜绝错误、漏洞与不可复现证明，数学知识将变得像软件一样可编译、可测试、可复用。
五、结论
陶哲轩以顶级数学家的视角，为当代AI的数学能力划出了清晰边界：
AI是两类工具的协同：生成式AI负责联想与检索，推理式AI（Lean）负责验证与保真；
AI有强能力但无理解力：擅长规模化、重复性任务，不具备原创思想与数学洞察；
AI不替代数学家，而是扩展数学家的能力边界，降低科研门槛；
数学研究范式正在革命：从小规模、手工、非形式化，走向大规模、协同、形式化。
这场革命不是AI战胜人类，而是人类使用AI，重新定义数学研究。
参考文献
[1] 陶哲轩. 在UCLA IPAM研究所AI for Science论坛的演讲[R]. 美国加州大学洛杉矶分校纯数学与应用数学研究所, 2026.
[2] Terence Tao. AI contributions to Erdős problems[EB/OL]. GitHub Wiki, 2026. https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems.
[3] Terence Tao. Recent progress on the Erdős problems[EB/OL]. 2025. https://terrytao.wordpress.com.
[4] Thomas Bloom. Erdős Problems Project[EB/OL]. https://erdosproblems.com/, 2023-2026.
[5] Song Peng, Yang Kai, Anima Anandkumar. Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean[C]//Proceedings of Machine Learning Research, 2025.
[6] 陶哲轩. 机器辅助证明与数学的未来[J]. 中国科学基金, 2025(01):45-51.
[7] 陶哲轩. 一次性解决一千个问题：AI如何改变数学研究[R]. 国际数学家联盟公众讲座, 2024.
[8] 陶哲轩. 形式化验证在AI数学中的关键作用[Z]. AI-Math社区论坛, 2024.
[9] 张钹, 朱军. 人工智能与数学交叉研究前沿评述[J]. 中国科学:信息科学, 2025, 55(3):521-540.
[10] 周志华. 机器学习与定理证明的协同路径[J]. 计算机学报, 2026, 49(1):1-18.
