数学与理论计算机科学的十大进展
Ten advances in mathematics and theoretical computer science
OpenAI 使用其下一代模型内部版本 Astra 解决十个数学问题，这些问题的“主要结果至少十年没有进展”，并声称在 GPT-5.6 Sol token 价格下每个问题花费不到 2000 美元。openai/ten-proofs 仓库包含 Lean 4 形式化证明、解决方案论文及 LLM 生成的证明重构 PDF。此前 Anthropic 用 Claude 的 Mythos Preview 发现密码学弱点，花费 10 万美元 token。Terence Tao 在《IEEE Spectrum》中描述“大数学”，设想人机协作的未来。
数学与理论计算机科学领域的十项进展。几天前，Anthropic 利用 Claude 的 Mythos Preview 发现了密码学弱点，花费了 10 万美元的 token，并在提示中写道“我们不是在寻找容易摘取的果实，我们想要真正的研究，以发现真正困难的发现”。现在轮到 OpenAI 展示实力了。他们让“我们下一个主要模型的内部版本 Astra”来解决十个数学问题，这些问题“主要结果至少十年没有进展”。他们声称在 GPT-5.6 Sol token 价格下，每个问题花费不到 2000 美元。（不过，没有消息透露有多少问题在未解决的情况下花费了 2000 美元。）openai/ten-proofs 仓库包含了他们结果的 Lean 4 形式化证明，还有一篇描述解决方案的论文，以及一个额外的 LLM 生成的 PDF，其中模型根据未发表的推理轨迹“重构了证明是如何形成的”。这展示了相当程度的透明度，但我想看到他们使用的提示！许多在线数学家正在经历一场集体性的“深蓝”时刻。OpenAI 的结果让我想起了 Terence Tao 在六月份《IEEE Spectrum》中描述的“大数学”：与一些同行不同，Tao 既不轻视 AI，也不畏惧它。相反，他视其为该学科根本性转变的催化剂——向他所称的“大数学”过渡。他设想了一个大规模、去中心化的人机协作未来，复杂的数学任务可以被切分和细分，人类负责创造性部分，而 AI 承担大部分技术性繁重工作。通过 Hacker News 标签：数学、AI、OpenAI、生成式 AI、LLM、深蓝