#数学研究

avatar
宝玉
12小时前
最近数学圈发生了一件很有意思的事。 世界顶级数学家陶哲轩在解决一个 Erdős（埃尔德什）的经典问题时，全流程都在用 AI 做助手——从证明草案，到简化证明，再到形式化验证。 Erdős 是20世纪最高产的数学家之一，一辈子发表了1500多篇论文，提出了无数开放问题。数学圈有个著名的"埃尔德什数"——如果你和他合作过论文，你的埃尔德什数就是1；和他的合作者合作过，就是2，以此类推。爱因斯坦的埃尔德什数是2。 后来有人专门做了一个网站，把他的很多未解决/已解决问题系统整理出来，这就是 Erdos Problems 网站。 陶哲轩讲的是其中的第 367 号问题，属于数论里的一个具体问题，专业数学研究级别的问题。 解决过程大概是这样的： 一位数学家 Wouter van Doorn 先给出一个人类手写的反例证明草案，但里面有一个关键恒等式他没完全证明，只是说：“相信有人能帮我确认一下”。 陶哲轩把这个恒等式扔给 Google 的 Gemini Deepthink 模式。大概十分钟后，Gemini 给出了一份完整证明，还顺带确认了整套论证是成立的。 Gemini 的证明用到了 p-adic 等比较高级的代数数论工具，对这个具体问题来说有点杀鸡用牛刀。于是陶哲轩花了半小时，把 AI 的证明手工转化成更基础、更易懂的版本。 两天后，另一位数学家 Boris Alexeev 用一个叫 Aristotle 的工具（基于 AI + Lean）完成了全套形式化证明，还特意手动检查最终结论，以防 AI 在形式化过程中存在编造。 陶哲轩觉得还没完，又用 Deep Research （同时用了 ChatGPT 和 Gemini）做了一轮文献搜索，看这个问题有没有前人类似工作。结果找到了若干关于连续幂数的相关论文，但没有直接解决第 367 号问题。 整个流程：人类提出猜想 → AI暴力证明 → 人类简化优化 → AI辅助形式化验证。 都在说 Gemini 3 已经到了博士生水平，看来所言非虚，这些事情真的需要数学博士级别才能做的出来，但另一方面，真正的数学家也并没有被 AI 代替：是人类决定哪个问题值得解决，是人类判断AI的p-adic方法太重了需要简化，是人类手工完成最终的形式化表述以验证 AI 的结果是否准确。 AI 做的是那些需要大量计算、符号推演、但方向已经明确的体力活。在 AI 时代，问对问题、甄别结果，比以前更重要了。
#陶哲轩 #AI辅助数学 #Erdős问题 #Gemini #数学研究
avatar
AI 辅助 Vibe Coding 也可以帮到陶哲轩（数学家） 「我利用了一次和 AI 的深入对话，来帮助回答了一个 MathOverflow 上的问题。 在此之前，我已经做过理论分析，倾向于认为答案是否定的，但我还需要一些数值参数去验证某些不等式，才能最终构造出反例。起初，我尝试让 AI 提供一段 Python 代码，用来搜索反例，然后自己运行和调整。但发现运行时间太长，而且最初的参数选择本来就注定会失败。 于是我改变策略，改为和 AI 一步一步对话，让它用一些启发式计算（类似试探的方法）来帮我找到更合适的参数。最后，AI 确实给出了可以使用的参数，我再单独进行验证（确实还是用它提供的 Python 代码，但这次只有 29 行，逻辑简单到我可以一眼看懂，并且算出来的数值也和之前的启发式推测吻合）。 在这个过程中，AI 工具帮我节省了大量时间——如果完全靠我自己做，可能要花上好几个小时写代码和调试。AI 不但利用上下文帮我发现并修正了请求中的数学错误，还在生成代码之前就解决了问题。实际上，如果没有 AI 的帮助，我几乎不可能去尝试这样的数值搜索，而是会直接走向理论上的渐近分析。」
AI高考数学测试：O3意外落后，Gemini夺冠引发热议· 62 条信息
#AI辅助 #Vibe Coding #陶哲轩 #数学研究 #MathOverflow