在数学研究的漫长历史中，人类智慧始终是推动学科发展的核心动力。然而，随着人工智能技术的飞速演进，特别是大语言模型在复杂推理领域的突破，数学研究的方法论正在经历一场静默而深刻的变革。近期，围绕著名数学家保罗・厄尔德什（Paul Erdős）遗留问题#367的解决过程，生动展现了AI如何从辅助工具演变为协作伙伴，并催生出“人类提出猜想-AI生成证明-专家优化验证”的新型研究范式。
这一事件始于厄尔德什问题网站（Erdős Problems）上编号#367的数学难题。该网站作为全球数学界的重要遗产平台，系统收录了厄尔多斯提出的数千个开放问题，涵盖数论、组合数学、图论等核心领域，持续吸引着专业研究者和数学爱好者参与攻克。独立研究者Wouter van Doorn于11月20日针对该问题第二部分提出了一个基于同余恒等式的反例构造，并在论坛中表达了“确信有人能够验证其成立”的期待。
关键转折发生在几小时后，当著名数学家陶哲轩将这一恒等式提交给谷歌最新发布的Gemini 2.5 Deep Think模型。这个专门针对深度推理任务优化的AI系统，在短短十分钟内不仅完成了恒等式的完整证明，更令人惊讶的是，其证明过程采用了p-adic代数数论等高等数学工具——虽然这些工具对该问题而言略显“过度复杂”，但充分展现了模型对抽象数学结构的深刻理解能力。
陶哲轩随后花费约半小时，将AI生成的证明“翻译”为更基础、更符合人类数学直觉的论证形式。这一步骤至关重要：它既验证了AI证明的逻辑正确性，又将其转化为数学共同体更易理解和接受的表述方式。更值得关注的是，陶哲轩指出该证明经过适当转化后，完全具备在Lean定理证明器中形式化的潜力——这为后续的机器验证奠定了基础。
两天后，数学家Boris Alexeev使用Harmonic的Aristotle工具，实际完成了该问题的Lean形式化工作。整个过程耗时两到三小时，最终产出了完全机器可验证的证明代码。特别值得注意的是，Alexeev选择手动形式化最终命题，这一谨慎做法既防止了AI可能存在的逻辑漏洞，也体现了当前人机协作中“人类保持最终控制权”的审慎原则。
这一案例的价值远不止于解决单个数学问题。它系统展示了AI在数学研究中的多重角色转变：从早期的计算辅助工具（如符号计算系统），到证明提示生成器（如GPT系列在启发式证明中的作用），再到如今能够独立完成非平凡证明的“协作者”。Gemini 2.5 Deep Think的表现表明，当前最先进的AI系统已能理解复杂的数学概念，组织多步骤推理，并选择适当的数学工具——尽管其选择可能不是最优或最优雅的。
更深层次看，这一事件揭示了数学研究流程的重构可能。传统上，数学证明的发现与验证都高度依赖人类专家的时间和精力。而AI的介入创造了新的分工模式：人类研究者专注于提出有意义的猜想和问题（如van Doorn的反例构造），AI负责探索证明路径和生成初步论证（如Gemini的快速证明），人类专家再对证明进行优化、简化和形式化验证（如陶哲轩的转化和Alexeev的Lean实现）。这种“猜想-证明-验证”的三阶段协作，显著提升了研究效率，同时保持了数学严谨性的最高标准。
值得注意的是，陶哲轩近年来持续探索AI在数学中的应用边界，从使用GPT-5 Pro处理不同尺度问题，到借助AlphaEvolve发现新的数学构造，再到通过ChatGPT加速开源项目开发，这些实践共同描绘出数学家与AI系统协同进化的路线图。而本次Erdős问题的解决，特别凸显了专门针对深度推理训练的模型（如Gemini 2.5 Deep Think）在严格数学证明方面的独特优势。
当然，挑战依然存在。AI生成的证明可能过度复杂或缺乏直觉解释性（如本案中不必要的p-adic工具使用），形式化验证仍需大量人工参与，且AI对数学美感和简洁性的把握仍远不及人类大师。但不可否认的是，数学研究正在进入一个前所未有的“增强智能”时代——不是AI取代数学家，而是数学家借助AI扩展自己的认知边界和问题解决能力。
展望未来，随着定理证明器与大型语言模型的进一步融合，以及专门针对数学推理训练的AI系统持续进化，我们有理由期待更多长期悬而未决的数学问题将通过人机协作获得突破。而厄尔德什问题#367的解决过程，将成为这一历史性转变的经典注脚，标志着数学研究从纯粹的人类智力活动，迈向人类与人工智能深度协同的新纪元。
关注“鲸栖”小程序，掌握最新AI资讯
本文由鲸栖原创发布，未经许可，请勿转载。转载请注明出处：http://www.itsolotime.com/archives/6397