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生成的数学发展已不可避免。
"大型AI生成的数学发展已不可避免。"
HN 评论区
- 有评论者指出，AI 在寻找反例方面表现优异，是因为机器没有对猜想的美学执念，也不担心生成‘丑陋’的反例而感到尴尬。
- 一位亲历者分享了数学界的故事：博士生发现教授证明存在缺陷，虽未直接解决猜想，但这一连接不同领域的发现仍助其毕业，后教授修正证明并与该生合作发表成果。
- 有从业者强调，大型语言模型并非针对每个任务单独训练，而是通过单一的 next token prediction 目标在多样化数据集上统一训练，从而获得跨任务迁移能力。
- 评论中提到，数学界缺乏发表‘负面结果’（如长期尝试未果但无法证明不可行）的传统，但这类软性结果对学科进步至关重要。
- 有观点认为，当前对 AI 能力加速的预测缺乏结构性依据，因为人类尚不理解 AI 能力的凸性，且其可能具有难以测量的涌现特性。