我用 AI 证明了 Conway 的猜想
I Vibed a Proof of Conway's Conjecture
作为数学新手，我花了整整一个月，利用 Claude 和 ChatGPT 等 AI 模型，尝试解决 John Conway 提出 50 年的 Omnific integers 猜想。起初，Claude 生成的内容充满华丽辞藻却缺乏实质，于是我切换策略，让 ChatGPT 扮演“怀疑者”角色进行批判性验证。通过这种“人机协作”的反复打磨，我最终在 Lean 系统中构建了一个机械验证通过的证明。虽然该证明尚未得到数学家的独立确认，但这一过程展示了 AI 在前沿数学探索中的独特潜力与协作模式。
我原本觉得在不理解数学本质的情况下“解决”问题很荒谬，但这恰恰让它变得格外诱人。
HN 评论区
290- gbjcantab
不知为何，这种做法让我想起某些奇幻魔法体系中“巫师”与“术士”的区别。“巫师”的魔法根本上建立在对奥秘事物的深入研究和理解之上，或许还会借助一些（必要或有益的）强大工具。“术士”则召唤超自然生物，能够控制、哄骗它们，并保护自己和他人免受其害（成功与否另说）……但真正产生所需魔法效果的其实是那些生物。
计算领域历史上一直属于“巫师”的范畴。看到这么多人如此拼命地朝“术士”的方向推进，甚至将这种“术士”手段应用到其他领域，而他们自己甚至无法验证咒语是否生效，这……挺有意思（？）的。
- bwfan123
> 无论哪种情况，我认为最能从 AI 中获益的仍然是数学家本人
数学的净产出将会增加，数学家们现在有更多工作要做，去解开这一切并使其变得有用。AI 扮演的角色类似于“无限猴子定理”[1] 中的猴子。我们现在需要一个针对 LLM 的推论——大概是这样的：给定无限的 token 预算，有限数量的 LLM 代理几乎必然能找到所有定理。
- pretzellogician
（背景：受过训练、发表过论文，但仍是业余数学家。）
这是一篇很酷的博文，我认为你走对了方向，并且在过程中开始理解这个证明了。
我建议你继续沿着简化和理解的路线走下去，直到你自己也能跟上证明的逻辑。基于我做过类似工作的经验，提几点建议：
1. 看看（或问问 AI）证明的各个部分是否能在别处找到，也就是说，某个论证是否只是对别处的复制？如果是，注明出处很重要，但这通常也能带来简化（例如“根据定理 X”等）。
2. 寻找冗余模式并尝试合并它们。
3. 让 AI 扮演某期刊的批判性审稿人，然后尝试修复它提出的批评。
4. 继续简化！假设最终结果实际上可能相对简短。
祝好运！
- unholiness
关于超实数及其周围博弈论概念的精彩入门介绍，可以参考这个关于 Hackenbush 的视频 [0]，它是 3Blue1Brown“数学之夏”竞赛的获奖作品。
[0]https://www.google.com/search?q=video+introduction+to+surrea...
- patcon
Prof Vincenzo Mantova[1] 的深层链接回复，他正在审查结果：https://news.ycombinator.com/item?id=49761718
[1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-manto...
- sigmar
> 我给一些数学家发了邮件，提出了一些可能的拼写错误修正，并得到确认，其中至少有几处修正确实是有效的。然而，有些未被 Lean 支持的问题，结果也被证明是误解。
我觉得这个项目真的很棒，但在你投入足够多的时间、能自称不仅仅是“业余爱好者”之前，就贸然给专家发冷邮件，这样做合适吗？OP 的邮件可能确实有帮助，但数十亿人都在用这些 LLM 涉足新领域，邮件的信号噪声比本来就低。
- Feathercrown
我发现作者与 LLM 的沟通方式非常迷人。例如：
> 然而，我并不想要任何结果；我想要那种能触动我的东西。
> 起初，我问了 Claude：
> 我：在超实数研究计划中，哪些未解问题最能触动你，为什么？
注意从“触动我”到“触动你”的转变。作者在这里对与 LLM 的关系/界限有何种认知？
1. 他们是否在使用它来寻找它标记为有趣的东西，希望这些东西也能让自己觉得有趣？
2. 他们是否认为“有趣”是一种普遍的（与观察者无关）特质，并利用 LLM 来寻找那些有趣的东西？
3. 他们是否已将寻找有趣事物的欲望委托给 LLM，让它去寻找它标记为有趣的东西，而不管作者本人的感受如何？
4. 他们是否将其视为自己思维过程的一部分，因此不区分“你”和“我”？
5. 他们是否将其视为自己的一部分，并用第二人称指代这个结合体？
我很希望能得到这方面的澄清。
- howunfortunate
> 第二天，出现了两个缺口：“无与零之间”和“零与无之间”。两个数字在这两个缺口处诞生。称它们为 -1 和 1。
我在这里就迷路了。我想我正式承认自己太笨了，不适合学数学。