导语：过去，人工智能在数学中的角色多是计算器、检索工具或公式助手；如今，它正逐步参与猜想发现、证明路线搜索、形式化验证和结果评议。🧠 从机器学习辅助数学家提出新关系，到大型语言模型生成可执行程序，再到系统完成奥数级证明，AI科研助手正在逼近真正的“研究合作者”。不过，一份机器生成的证明能否成为数学知识，仍要经过专家审查、形式化核验与同行评审，而不能只看模型给出的答案是否流畅。
从发现规律到提出可研究的猜想
AI进入数学研究的早期突破，并不是直接证明著名猜想，而是从海量数据中寻找人类不易察觉的联系。2021年发表于《自然》的研究展示了一套“机器学习引导数学直觉”的方法：模型先分析数学对象之间的潜在关系，再由数学家解释模式、提出猜想并完成证明。相关工作在纽结理论和表示论中形成了有意义的新结果，说明AI最初扮演的是“放大观察力”的科研助手。读者可参阅《自然》论文[1]。
这种协作模式的重要价值，在于把AI的模式识别能力与数学家的概念理解结合起来。模型可以快速筛选变量、计算样例和比较结构，但“为什么某个关系值得研究”“它与现有理论有何联系”等问题，仍需要领域知识判断。🔍 因此，破解猜想的第一步往往不是让模型立刻写证明，而是要求它生成候选命题、搜索反例，并明确每个结论的适用范围。
可执行搜索让数学发现更容易核验
2023年公布的FunSearch进一步改变了工作方式。该系统让大型语言模型生成程序，再通过自动评估器运行、打分和筛除错误方案，随后不断改进高分候选。研究团队将其用于组合数学中的帽集问题，找到超过既有结果的新构造，同时在在线装箱问题上发现了更有效的启发式算法。相关成果经过学术发表，详见《自然》论文[2]和项目说明[3]。
FunSearch的关键不只是“模型想出了答案”，而是候选方案能够被程序直接执行和评分。✅ 这为控制幻觉提供了实用途径：语言模型负责提出多样化思路，确定性评估器负责淘汰不满足条件的结果。不过，“找到更优构造”与“证明对所有情形成立”仍属不同层次，前者可通过计算核验具体对象，后者则需要完整的逻辑链条。
形式化证明成为机器推理的安全护栏
在证明任务中，自然语言最容易隐藏跳步、概念偷换和边界条件遗漏。Lean等交互式定理证明器要求研究者把定义、前提和推理步骤写成精确的形式语言，再由内核逐步检查。Lean官方资料指出，计算机既可以帮助寻找证明，也能帮助验证候选证明；通过内核检查意味着证明项符合当前定义、定理和公理，但仍须确认形式化命题准确表达了原始问题。可参考Lean定理证明导论[4]及证明验证说明[5]。
2024年，AlphaProof与AlphaGeometry 2在国际数学奥林匹克竞赛题上达到银牌水平，六道题中解决四道；其中AlphaProof采用形式化数学语言和强化学习寻找证明。2025年，Gemini Deep Think进一步以自然语言端到端处理题目，在官方评分中达到金牌标准。📐 这些进展表明，AI已经能处理长链推理与非显然构造，但竞赛题通常已有确定答案和较清晰的评判标准，与真正未知的开放猜想仍存在距离。相关信息见2024年项目报告[6]和2025年官方评测说明[7]。
机器生成证明如何接受同行评审
机器证明的同行评审不能只问“代码是否通过”，而应建立多层审查。第一层是数学审查，检查论证结构、关键引理和文献关系；第二层是形式化审查，确认代码没有未完成占位、非必要公理或绕过内核的操作；第三层是语义审查，核对形式化命题是否与论文声称的猜想一致；第四层是复现审查，记录模型版本、提示词、依赖库、随机种子和运行环境。只有这些材料可以独立复现，评审者才能判断成果究竟来自数学创新、计算搜索，还是设定偏差。
“通过证明检查器”不等于“已经完成同行评审”；它证明的是某个形式陈述可由指定前提推出，而同行评审还要判断问题表述、创新性、已有工作、解释质量和研究价值。
期刊和会议还需要处理作者责任问题。AI不能像人类作者一样承担学术责任，因此更合适的做法，是由研究者署名并完整披露AI参与环节，例如文献整理、引理生成、反例搜索、形式化编码或语言润色。若关键证明由模型生成，论文应提供原始输出、人工修改记录和失败路线摘要，让评审者能够识别潜在的数据记忆、循环引用与选择性报告。🧾
科研团队可以采用的实用流程
- 先固定问题：写清定义、量词、边界条件和允许使用的定理，避免模型在不同版本的猜想之间切换。
- 并行探索路线：分别让AI尝试归纳、反证、构造、概率方法和反例搜索，而不是反复改写同一思路。
- 设置对抗检查：由独立模型或研究者专门寻找最小反例、隐含假设与不成立的中间引理。
- 逐步形式化：先验证核心引理，再连接完整证明，防止自然语言中的小错误累积成结构性漏洞。
- 保留研究日志：保存提示词、模型版本、代码、依赖项和人工决策，使结果能够被第三方复查。
- 提交双轨材料：同时提供人类可读论文与机器可检查证明，兼顾理解、验证和长期维护。
总结：AI正在改变证明生产，而非取消数学判断
AI科研助手的新进展，核心并非“模型是否已经取代数学家”，而是数学发现正在形成新的流水线：AI扩大搜索空间，程序评估器筛选候选方案，形式化系统检查逻辑，人类专家负责解释、归因和评价。🚀 未来真正有影响力的成果，很可能不是一段突然出现的“完美证明”，而是一套公开、可复现、可审计的证据链。对于尚未经过独立核验的所谓“著名猜想已破解”消息，最稳妥的态度仍是区分候选证明、形式化验证、专家认可与正式同行评审，并等待数学共同体完成必要的复查。
