人类数学家正被“反例碾压”

AI 反例结果的范围

• 讨论集中在一个由 LLM 辅助发现的雅可比猜想反例（7 次、3 个变量、2026）。
• 有人认为这并不算根本性的新东西：几十年来计算机一直被用于寻找反例；如果技巧和算力足够，LLM 之前的系统也许也能找到类似例子。
• 也有人说，关键的新意在于：同一个通用模型如今能同时做高等数学、写代码、写作和推理，而不是只会做某个狭窄的专家系统。

AI 与人类各占多少作用？

• 有人强调，仍然是数学家选择了问题、将其形式化并设计了搜索；在一次复现中使用的提示词虽然通用，但并不简单。
• 怀疑者强调人类的强力引导、漫长的代码运行和证明检查；并警惕把“AI 解决了 X”这类标题过度炒作。
• 支持者反驳说，这正是人类协作的方式，而模型如今能够自主设计针对巨大空间的、并不天真的搜索。

LLM 的训练与通用性

• 讨论集中在模型是否是“针对每个任务分别训练”的问题上。
• 一方认为，经典 AI 需要为不同任务分别设计架构和数据集。
• 另一方认为，现代 LLM 只用单一的下一个 token 目标在多样数据上训练，配合 RL 让能力浮现；任务表现是涌现出来的，而不是分别单独训练出来的。

反例在数学中的意义

• 许多人指出，反例至关重要：它们能修正猜想、收紧定理表述，并填充“病态案例”的“图鉴”。
• 有些人觉得反例并不令人满足，因为它们没有解释直觉为何失效；他们想要的是结构性洞见，而不只是一个反驳。
• 也有人认为，发现任何一个决定性的反例本身就已经极具价值，尤其是对于长期悬而未决的猜想。

形式化、证明检查与错误

• 讨论涉及 Lean 和其他证明助手：AI 可以生成大规模形式化证明；人类可能只需要理解定义和定理链条，而不必逐个理解每个引理。
• 有人担心数学本身就充满了未被注意到的错误；形式化项目旨在逐步验证整个知识体系。
• 也有人担忧未来会出现大量 AI 生成的“证明”，如果没有机械化验证，人类实际上无法现实地逐一检查。

更广泛的影响、可及性与伦理

• 有人推测，类似方法还会攻克其他深层猜想，随后是理论物理和计算机科学，尤其是在验证成本较低的领域。
• 有些人认为，为强模型付费使用对研究生来说是合理投资；另一些人则基于伦理（数据、环境）或智识上的原因拒绝使用 LLM。
• 乐观观点认为，AI + 人类可以成为“好团队”，让资源不足的研究者也能借助优秀模型与外部人士进行有意义的合作。