On August 1, 2026, OpenAI said an internal version of its next model, Astra, solved ten open problems in mathematics and theoretical computer science. The tokens used to find the solutions would cost about $2,000 at API rates.

Claims like this are usually impossible to check. This one is different. OpenAI published every proof as a Lean 4 certificate on GitHub. So I downloaded them and looked.

Why This Announcement Is Checkable

Most AI research claims arrive as a PDF and a benchmark score. You either trust the lab or you don’t.

Lean is different. Lean is a proof assistant — a programming language where you write mathematical proofs, and a compiler checks every single step. If one step does not follow from the previous one, the build fails. There is no “looks right to me.”

This matters because it removes the model from the trust chain. You do not have to believe Astra reasoned correctly. You only have to believe the Lean compiler works — and it is already the tool the formal-mathematics community builds on, through the mathlib library.

The Ten Results

From the repository’s own README:

#ResultField
1Improved asymptotic upper bounds on sphere-packing density, reaching the Cohn–Elkies thresholdHigh-dimensional geometry
2Exponentially stronger upper bounds for binary codes at every minimum distance, plus spherical codesCoding theory
3A construction of a non-sofic groupGroup theory
4A counterexample to Connes’s rigidity conjectureOperator algebras
5New lower bounds for computing the permanent, including an n⁴ / log n formula lower boundCircuit complexity
6Exponential parallel repetition for arbitrary finite two-player quantum gamesQuantum complexity
7Polynomial-factor hardness of approximation for the closest vector problemLattice cryptography
8The sharp maximum volume for a convex body whose centroid is its only interior lattice point (Ehrhart’s volume conjecture)Convex geometry
9A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183Combinatorics
10Counterexamples to the compactness and degeneracy conjectures, resolving Erdős problems 146 and 180Extremal graph theory

Result 1 deserves a note. The standard upper bound on sphere-packing density in high dimensions comes from Kabatiansky and Levenshtein in 1978, and has the form 2^(-(0.599...+o(1))n). Later work sharpened the constant in front, but that exponential rate has stood for nearly fifty years. Press coverage describes Astra’s result as the first real improvement to it — OpenAI’s own README says only “reaching the Cohn–Elkies threshold,” so treat the stronger framing as reporting, not as the lab’s claim.

What I Found in the Repository

The repo is openai/ten-proofs. GitHub’s API says it was created 2026-08-01 at 06:10 UTC, licensed Apache-2.0.

Here is what is actually inside:

git clone --depth 1 https://github.com/openai/ten-proofs.git
cd ten-proofs

# How many Lean files, and how big?
find . -name '*.lean' | wc -l          # 23
find . -name '*.lean' -print0 | xargs -0 cat | wc -l   # 549,980

23 Lean files. About 550,000 lines. That is not a sketch. That is a formalization effort at industrial scale.

The sorry check

In Lean, sorry is the escape hatch. It tells the compiler “assume this step, I’ll prove it later.” Any proof containing sorry is incomplete. It is the first thing you grep for when someone hands you a formalization.

grep -rn --include='*.lean' '\bsorry\b' . | wc -l    # 42

Forty-two. That looked bad. But look at where they are:

# Outside the ComparatorChallenges directory:
grep -rn --include='*.lean' '\bsorry\b' . | grep -v ComparatorChallenges | wc -l   # 0

Zero sorry in the actual proofs. All 42 sit inside ComparatorChallenges/, which is a different thing entirely — and it is the most interesting part of the repository.

What ComparatorChallenges actually does

Each challenge is a pair: a .lean file and a .json config, wired to Comparator. Here is a real config, D_NonSoficGroup.json:

{
  "challenge_module": "ComparatorChallenges.D_NonSoficGroup",
  "solution_module": "NonSoficGroup",
  "theorem_names": ["SoficGroups.SourceTopLevelCompressionFinal.exists_finitelyPresented_nonsofic_group"],
  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
  "enable_nanoda": true
}

That closes three different escape hatches at once:

  1. The statement can’t drift. The challenge file re-defines every concept from scratch — Sofic, PermutationModel, and the rest — instead of importing the solution’s definitions. So the proof has to satisfy an independently written statement. A formal proof can be perfectly valid and still prove the wrong theorem if the statement was written loosely; this is the guard against that.
  2. No smuggled axioms. permitted_axioms allows only Lean’s three standard ones. You cannot quietly axiom myLemma : ... your way to a result. I checked all twelve configs — every one lists exactly those three, and there are zero custom axiom declarations anywhere in the proof files.
  3. No trusting Lean’s own kernel. enable_nanoda: true re-checks the proof with nanoda, a separate Lean kernel implementation. If Lean’s kernel had a soundness bug, an independent one has to agree.

So the sorry in those files is deliberate: it is the hole the solution must fill. There are twelve challenge configs for ten results, because two results are split into two statements each.

I also checked for admit, Lean’s other way to skip a step. Zero.

Checking it yourself

The project pins Lean 4.32.0 with mathlib and Lake:

# with elan installed
lake exe cache get      # fetch prebuilt mathlib
lake build All          # build all ten formalizations

Be warned: building mathlib-scale Lean is slow and memory-hungry. lake build SpherePacking builds a single result if you just want one.

What This Does Not Mean

The proofs being real does not make every version of the headline true.

The $2,000 is a publication cost, not a discovery cost. It counts the tokens for runs that worked. It does not count failed attempts, and it does not count the humans.

Humans were in the loop. OpenAI staff helped prepare the manuscripts and formalize the arguments. The model did not wake up, solve ten problems, and push to GitHub unattended.

OpenAI chose which results to show. We are seeing the selected wins, not the full attempt log.

Astra is not released. This was an internal version. Nobody outside OpenAI can reproduce the search that found these proofs — only verify the proofs that came out. That is a meaningful gap: the artifacts are open, the process is not.

Reactions split along exactly that line. Fields Medalist Timothy Gowers said he would recommend one of the proofs to a top journal. Thomas Bloom, who maintains the Erdős problems catalogue, called the results big news. Critic Gary Marcus called them “amazing but vastly oversold.” All three can be right at once.

Why Developers Should Care

You are not going to formalize a Ramsey number this week. But the pattern here is one you will meet soon.

The interesting move is not “AI did math.” It is “AI output shipped with a machine-checkable certificate attached.”

That is a template. When a model writes something you cannot personally audit, the question stops being do I trust the model and becomes what artifact did it produce that a machine can check without trusting it?

You already have cheap versions of this:

# The model wrote code. Don't review the vibes — check the artifact.
mypy --strict src/          # types are a proof the compiler checks
pytest -q                   # tests are a claim you can run
cargo build                 # the borrow checker doesn't care how confident it was

Same shape, lower stakes. A type checker is a very small proof assistant. The stronger your checkable artifact, the less the model’s confidence matters — and model confidence is the thing you should trust least.

This is also the honest counterweight to the Anthropic evaluation incidents from last week. A model that talks itself into the wrong conclusion is dangerous exactly when nothing external can check it. Astra’s proofs are the opposite case: the model’s reasoning could have been sloppy anywhere along the way, and the compiler would have caught it.

Sources: Ten advances in mathematics and theoretical computer science (OpenAI, August 1, 2026) · openai/ten-proofs — repository inspected directly on August 4, 2026.