LLM 突破 10 个十年数学难题，附 Lean 4 形式化证明

2026 年 8 月 1 日——链接博客

数学与理论计算机科学的十项进展（来源）几天前，Anthropic 才刚刚使用 Claude 和 Mythos Preview 发现了密码学弱点，为此花费了价值 10 万美元的 token。他们使用的 prompt 中还包括这样一句话：“再次强调，我们要找的不是唾手可得的成果，而是要进行真正的研究，找出确实很难发现的问题。”

现在轮到 OpenAI 展示实力了。他们让“内部版本的 Astra，也就是我们的下一代重大模型”去寻找十道数学难题的解法。这些问题“至少十年来，其主要结论都没有取得任何进展”。他们声称，按 GPT-5.6 Sol 的 token 价格计算，每道题的花费都不到 2,000 美元。

（不过，他们没有透露还在多少道题上花了 2,000 美元，却没能找到解法。）

openai/ten-proofs 仓库中提供了这些结果的 Lean 4 形式化证明；此外还有一篇描述解法的论文，以及一份由 LLM 生成的 PDF。模型根据未公开的推理轨迹，在这份 PDF 中“重构了整个证明是如何形成的”。

这种透明度已经相当不错了，但我还是想看看他们使用的 prompt！

网上许多数学家正在集体经历一场“Deep Blue 时刻”。

OpenAI 的这些成果让我想起了 Terence Tao 今年 6 月在 IEEE Spectrum 中所描述的“big mathematics”：

与一些同行不同，Tao 既不排斥 AI，也不惧怕它。相反，他认为 AI 将推动这一学科发生根本性转变——迈向他所谓的“big mathematics”。他设想的未来，是人类与机器开展大规模、去中心化的协作：复杂的数学任务可以被拆解、细分，人类负责其中富有创造性的部分，而 AI 则承担绝大多数繁重的技术工作。

Stateless MCP 再次引起了我的兴趣（并启发了 mcp-explorer 和 datasette-mcp）——2026 年 7 月 31 日

OpenAI 对 Hugging Face 发起的意外网络攻击，是已经成为现实的科幻故事——2026 年 7 月 22 日

与 Claude Code 团队的 Cat 和 Thariq 炉边对谈——2026 年 7 月 21 日

这是一篇由 Simon Willison 发布的链接文章，发布于 2026 年 8 月 1 日。

每月赞助我 10 美元，即可收到一封精心整理的邮件摘要，汇总当月最重要的 LLM 进展。

花钱让我少给你发点内容！