- ChatGPT 推翻了埃尔德什单位距离猜想；数学家们证实了这一点，但最初没有在 Lean 中形式化。
- Logical Intelligence 在 Lean 中自动形式化了反例，鲍里斯·阿列克谢夫利用 OpenAI 的 Sol 模型实现了完整的 Lean 形式化，三周内生成了 120 万行 Lean 代码。
- 在一次研讨会上，一篇关于有限平坦群概形的 AI 生成论述包含了一个错误主张；AI 识别并为此提供了反例。
- AI 通过 Sol 和 Fable 发现了格罗滕迪克关于阶为 n 的群概形问题的反例。阿基尔·马修在 Lean 中将其形式化，并加入了 mathlib。
- Sol 和 Fable 等 AI 工具加速了数学项目的形式化进程，例如模性提升定理，并正成为研究人员不可或缺的助手。
- Fable 发现了长期未解的雅可比猜想的一个反例。保罗·勒泽奥将其形式化，DeepMind 的存储库促进了验证过程。
- AI 生成的数学需要形式化验证以确保可信，但理解反例带来的洞见仍是人类数学家面临的核心挑战。