数学和理论计算机科学的十项进展
摘要
OpenAI 使用内部模型 Astra 解决了十个长期未取得进展的数学问题，并公开了形式化证明和论文，每个问题花费不到 2000 美元的 token 成本。
核心要点
- 所用的模型是 OpenAI 内部版本 Astra，并非对外公开的模型。
- 被解决的十个数学问题均“至少十年未见主要结果进展”。
- 每个问题花费不到 2000 美元，价格基于 GPT-5.6 Sol token 计算。
- 结果已开源至 openai/ten-proofs 仓库，包含 Lean 4 形式化证明。
- 同时发布了一篇论文和一份 LLM 生成的 PDF，用于重建证明的推理过程。
原文佐证
- They set "an internal version of Astra, our next major model" on finding solutions to ten mathematical problems that "have seen no progress on the main result for at least a decade". They claim to have spent less than $2,000 at GPT-5.6 Sol token prices on each one.
- He envisions a future of large-scale, decentralized collaborations between humans and machines, where complex mathematical tasks can be diced and sliced, with humans claiming the creative parts and AI doing the lion’s share of the technical grunt work.
AI 洞察
这一成果表明，顶尖 AI 模型已能在纯数学领域产生实质性突破，并以极低成本进行形式化验证。对数学界而言，这类似深蓝之于国际象棋，可能推动学科向人机协作的“大数学”范式转变，同时引发关于数学本质和研究者角色的深层讨论。若这一能力持续演进，AI 或将在更多未解难题上超越人类极限。