ChatGPT与Sol接连推翻数学猜想
Human mathematicians are being outcounterexampled
最近几周，数学界发生了翻天覆地的变化。ChatGPT先是否定了Erdős的单位距离猜想，随后Logical Intelligence利用Lean完成了自动形式化验证。紧接着，OpenAI的新模型Sol在短短三周内生成了120万行Lean代码，不仅形式化了该反例，还攻克了全局类域论的难题。在Formalizing Fermat研讨会上，AI工具Logos和Claude Fable更是联手发现了一个关于Grothendieck猜想的反例，即存在一个阶为4却不被4整除的群概型。从ChatGPT到Sol，AI不仅找到了反例，还能在Lean中自动完成形式化证明，这标志着人类数学家正在被AI“反例化”，大型AI生成的数学发展已不可避免。
HN 评论区
252- Dove
读研时，我有机会旁听导师的一门课，他会在课上讨论自己的最新研究和一些未解问题。那是一个相对容易入门的领域，有些问题甚至简单到我们可以做出有意义的贡献。
某个周五下午，他提出了一个猜想，希望它是真的，并邀请我们尝试帮他证明或证伪它。这是他真心希望成立的东西；他喜欢平滑、优美的数学结构。而我则希望它是假的，因为我喜欢数学中那些古怪和例外的东西。此外，我完全不懂证明这类命题所需的工具，但我当然可以寻找反例。
周一我得知，他整个周末都在尝试证明这个猜想，但失败了。而我则把所有精力都用来寻找反例，不到一小时就找到了一个。
我对数学研究的唯一（虽然很小）的贡献就是这个反例，因为这是我唯一能做的事。不过这个故事确实说明，让拥有不同工具、期望和动机的人共同研究一个问题，是有帮助的。我过去不是，将来也永远不会成为那位伟大数学家的影子，但在当时，我有理由朝与他不同的方向探索。
- hintymad
> 雅可比猜想（Jacobian Conjecture）
有趣的是，以孪生素数猜想闻名的张益唐曾在普渡大学师从 Tzuong-Tsieng Moh，花了 7 年时间研究雅可比猜想。他论文中的关键一步用到了 Moh 的一个推论。结果发现，这个推论是错误的。因此，Moh 拒绝为张益唐写任何推荐信，张益唐也找不到任何教学或研究工作，最终在 Subway 打工多年 [1]。
想象一下，如果张益唐在 1986 年开始研究雅可比猜想时就有 ChatGPT 会怎样。
[1] 当然，如今这已变成一个励志故事。不过，这个故事确实引发了复杂的情感。或许用这首中国诗来形容最合适，但我实在不知道该怎么翻译：庾信平生最萧瑟，暮年诗赋动江关
- satvikpendem
这是件好事。它让人们不再浪费时间试图证明那些已知为假的东西，从而可以将精力转向其他值得证明的命题。至少在数学领域，这是对人类社会时间更有效的利用。
- vlovich123
> 几天前，我收到帝国理工学院数学系一位教授发来的邮件，他对一些研究生每月支付 200 美元以访问 Sol 和 Fable 等模型表示惊讶。他说他认为这些人疯了。我当时没有立即回复。但在与 Andrew 会面后，我回信给那位教授，告诉他在我看来，任何不每月支付 200 美元来使用这些工具的博士生才是疯了。事实上，在研讨会期间，我从哈佛博士生 Bryan Wang 那里得知，哈佛已经向所有博士生、博士后和教职员工免费提供 Fable 的访问权限。
是的，鉴于这些工具能极大加速研究生产出有意义的成果，为什么不每年为每位学生投入 2400 美元呢？总体而言，这简直是小钱。
- FabHK
顺便说一句，数学中的反例非常重要，往往有助于精炼定义并完善证明。
1) 我强烈推荐 Imre Lakatos 1976 年出版的精彩著作《证明与反驳》（Proofs and Refutations）。
2) 还有相当多专门讨论反例的书籍，例如在拓扑学、概率论、分析学等领域。
- dzdt
我想，由 AI 来创作数学版的《约翰·亨利之歌》（The Ballad of John Henry）也是迟早的事。谁将是那位人类冠军，那位能写出机器无法超越的“来自书中”（from the book）证明的最后一位伟大英雄？
- slibhb
> 一位我不愿具名的教员对我表示，反例如此容易被找到，恰恰说明人类在这个问题上思考得不够，暗示 Grothendieck 提出的那个 60 年的问题其实并不值得研究。我没有告诉他，在我职业生涯的某个阶段，我曾为此问题苦思了一周。在我看来，我的同事正经历哀伤的五个阶段；目前看来，他正处于否认阶段。
在我看来，那些极力反对 LLM 的人似乎也正处在哀伤的否认阶段。
- angry_octet
真希望我在大学时就有基于 LLM 构建的 Lean 形式化证明，因为幻灯片里的数学内容错误百出，而有些教授非常糟糕，不愿承认错误，同时却以“证明就在幻灯片里”为由拒绝学生的澄清请求。
当然，Lean 证明很少是理解证明的好方法，但希望它们能用来生成更易被人类理解的论证。