数学家被 AI 反例打得措手不及

Human mathematicians are being outcounterexampled

Kevin Buzzard 回顾了过去几周 AI 在数学形式化里连续找出反例的事。5 月 ChatGPT 用数论定理推翻了 Erdős 单位距离猜想；Logical Intelligence 在一周内把整篇论文自动转成了 Lean 代码。6 月 OpenAI 的 Boris Alexeev 用新模型 Sol 从公理出发完成了完整的形式化，生成了 120...

推荐理由：Kevin Buzzard 用第一人称给出了最近 AI 在形式化数学里连续找出反例的时间线，从 ChatGPT 推翻 Erdős 猜想到 OpenAI Sol 从公理出发完成形式化，细节扎实、叙事有张力，值得放在 featured。分数没拉满是因为这更像一篇个人观察和阶段性记录，正文没给出这些反例是否经过同行复核、模型在更广泛数学问题上的泛化表现也没展开。