---
title: "OpenAI's Internal Astra Model Solves Ten Math Problems for Under $2,000 Each"
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","Big Mathematics","Mathematical Proof"]
---

# OpenAI's Internal Astra Model Solves Ten Math Problems for Under $2,000 Each

## AI commentary

> The real takeaway isn't that AI solved a few problems—it's that the cost dropped below $2,000, making automated mathematical discovery economically viable for everyday use. For mathematicians and AI researchers, the missing prompts and failure data are the biggest mystery; I'd recommend checking the original repo and paper for details.

## At a glance

Following Anthropic's cryptographic discovery with Claude, OpenAI has showcased its next-generation model Astra by making breakthroughs on ten mathematical problems that had seen no progress for at least a decade, spending under $2,000 per problem at GPT-5.6 Sol token prices. OpenAI released Lean 4 formalizations, a paper, and an LLM-generated PDF reconstructing the proof process from unpublished reasoning traces, offering decent transparency—though the prompts remain undisclosed. Mathematicians online are experiencing a collective 'Deep Blue moment.' Terence Tao's vision of 'big mathematics' describes AI as a catalyst for large-scale, decentralized human-machine collaboration, with humans handling creative aspects and AI doing technical grunt work.

## Key points

- OpenAI used its internal Astra model to solve ten math problems stalled for over a decade, with token costs under $2,000 per problem.
- The project open-sourced Lean 4 formalizations and a paper, plus an LLM-generated PDF reconstructing the proof process.
- Prompts were not disclosed, and mathematicians online are calling it a 'Deep Blue moment.'

## Full text

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

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_80a4db1af93c388f2bb405c3