---
title: "OpenAI 内部 Astra 模型攻克十道数学难题，成本低于 2000 美元"
source: "Simon Willison 博客（Atom）"
source_tier: "t2"
url: "https://simonwillison.net/2026/Aug/1/ten-advances-in-mathematics/#atom-everything"
permalink: "https://feed.astralor.com/items/itm_80a4db1af93c388f2bb405c3"
published: "2026-08-01T20:34:49.000Z"
score: 68
channel: "ai"
tags: ["Astra","Lean 4","OpenAI","大数学","数学证明"]
---

# OpenAI 内部 Astra 模型攻克十道数学难题，成本低于 2000 美元

## AI 点评

> 这则新闻真正值得关注的点不是 AI 解了几个题，而是成本降到了 2000 美元以下——这让自动化数学发现第一次具有了日常可用的经济性。对数学家和 AI 研究者来说，提示词与失败数据的缺失是最大悬念，建议去翻原仓库和论文核对细节。

## 速览

继 Anthropic 用 Claude 发现密码学弱点后，OpenAI 也展示其下一代模型 Astra 的实力：在十个至少十年无进展的数学问题上取得突破，每个问题耗费的 token 成本不到 2000 美元。OpenAI 公开了 Lean 4 形式化证明、论文以及由模型根据推理轨迹生成的复盘 PDF，透明度较高，但未披露提示词。数学家群体对此反应类似“深蓝时刻”。陶哲轩曾提出“大数学”愿景，认为 AI 将成为人机协作解决复杂数学问题的关键催化剂。

## 关键点

- OpenAI 用内部 Astra 模型解决了十个搁置超过十年的数学难题，单个问题 token 成本低于 2000 美元。
- 项目开源了 Lean 4 形式化证明和论文，并附有模型基于推理轨迹生成的复盘 PDF。
- OpenAI 未公布具体提示词，数学家们惊呼这是 AI 的“深蓝时刻”。

## 全文

Ten advances in mathematics and theoretical computer science A few days ago it was Anthropic discovering cryptographic weaknesses with Claude using Mythos Preview, spending $100,000 on tokens and with prompts that included "again we are not looking for low hanging fruit, we want proper research to find genuinly hard findings." Now it's OpenAI's turn to flex. 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. (No news on how many problems they spent $2,000 on without reaching a solution though.) The openai/ten-proofs repository has Lean 4 formalizations of their results, and there's also a paper describing the solutions and an additional LLM-generated PDF where the model "reconstructs how the proof came together" based on the unpublished reasoning traces. That's a decent level of transparency, but I want to see the prompts they used! A lot of mathematicians online are experiencing a collective burst of Deep Blue. OpenAI's results reminds me of what Terence Tao described as "big mathematics" in IEEE Spectrum in June: Unlike some of his peers, Tao is neither dismissive of AI nor fearful. Instead, he sees it as the catalyst for a fundamental shift in the discipline—a transition toward what he calls “big mathematics.” 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. Via Hacker News Tags: mathematics, ai, openai, generative-ai, llms, deep-blue

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_80a4db1af93c388f2bb405c3