Ten Proofs You Can Actually Run

On August 1, 2026, OpenAI published a Git repository. That sentence sounds mundane until you read what is inside it: ten mathematical results, each with a Lean 4 formalization, a reasoning walkthrough, and a build command. The results include a non-sofic group, a counterexample to Connes's rigidity conjecture, quantum parallel repetition, and seven more. Sébastien Bubeck announced them as proofs from Astra, which he described as OpenAI's next major model. Noam Brown said an internal version of Astra had solved ten open problems across mathematics, quantum complexity, and theoretical computer science.

The headline everywhere was "AI solved ten open problems." That is the version that travels. The version that matters more is the one sitting on GitHub: named Lean modules, a lake build instruction, a formalization metadata file, and Comparator challenge configurations. These are proof objects you can clone, inspect, and compile yourself.

What the repository actually contains

The repository at github.com/openai/ten-proofs has a straightforward structure. There are ten named Lean modules, each corresponding to one stated result. An All.lean file aggregates them. A formalization.yaml file specifies the toolchain: Lean 4.32.0, mathlib, and Lake as the build system. The axioms listed are the standard three: propext, Classical.choice, and Quot.sound. Nothing exotic.

The README gives two commands: lake exe cache get to fetch prebuilt mathlib artifacts, then lake build All. You can build individual modules if you want to check one result at a time. There is also a ComparatorChallenges/ directory containing configuration files for independent verification challenges.

Alongside the code, OpenAI released a research paper and a separate reasoning walkthroughs document. The walkthroughs are meant to bridge the gap between the Lean certificate and the human-readable mathematical argument. A Lean file confirms that a formal statement has been derived from axioms. It does not explain why the proof idea works or whether the formal statement faithfully captures the mathematical claim. The walkthroughs address that second layer.

The ten results

The README lists the following:

1. High-dimensional sphere-packing bounds
2. Stronger binary and spherical-code bounds
3. A non-sofic group
4. Counterexample to Connes's rigidity conjecture
5. Arithmetic-circuit and formula lower bounds for the permanent
6. Quantum parallel repetition
7. Polynomial-factor hardness for closest vector problem approximation
8. Ehrhart's volume conjecture
9. Multicolour triangle Ramsey lower bound
10. Counterexamples to extremal graph-theory compactness and degeneracy conjectures

Some of these are the kind of result that would make a career. A non-sofic group has been a known target in group theory for years. Connes's rigidity conjecture has been a central question in operator algebras. Ehrhart's volume conjecture connects combinatorics and convex geometry.

The range matters too. These are not ten variations on one theme. They span geometric combinatorics, group theory, operator algebras, circuit complexity, quantum information theory, lattice problems, and extremal graph theory. Whatever process produced them is not narrow.

What Lean certification means

This is where the public conversation got fuzzy.

A Lean certificate says that a formal statement, expressed in Lean's type theory, has been derived from the listed axioms using valid inference rules. The checking is mechanical. If lake build succeeds on your machine, the derivation is valid according to the Lean kernel. There is no judgment involved in that step. The type checker either accepts the derivation or it does not.

But three questions remain outside what the certificate settles.

First: does the formal statement in Lean correspond to the mathematical claim as understood by mathematicians? A formalization can be technically faithful to its own wording while subtly differing from the problem people actually care about. This is why the paper and the walkthroughs matter. They give mathematicians the mapping between the informal claim and the formal one.

Second: is the proof interesting? A certificate confirms validity. It says nothing about whether the method introduces a new idea, combines existing techniques in a surprising way, or just grinds through a computation. The mathematical community will need time to assess this.

Third: what role did people play? Selecting which ten problems to attempt, translating informal statements into Lean, and editing proof scripts are all activities where human judgment could shape the outcome. OpenAI has not yet detailed the division of labor in its announcement materials.

None of these qualifications diminish the repository. The formal artifacts are real, they are checkable, and they open a set of questions that a press release alone could not open.

The reactions worth reading

The announcement thread on X drew reactions ranging from astonishment to skepticism. The most useful comments came from researchers who pressed on the gap between a valid certificate and a settled mathematical question.

Several people pointed out that we do not yet know the denominator. How many problems were attempted and failed for every one that was solved? What was the compute cost per successful proof? Without those numbers, it is hard to calibrate the significance of ten successes.

Others noted that the formalization step is itself a significant human contribution. Writing a faithful Lean statement for an open problem in operator algebras requires deep understanding of both the mathematics and the proof assistant. The formalizer is doing intellectual work that the certificate cannot capture.

A few respondents dismissed the announcement because Astra itself is not publicly available. That position understates what has been released. The proofs are open even if the model is closed. Anyone with Lean installed can verify them. That is a different kind of openness from "trust the benchmark score."

Why the release shape matters

AI research claims have an archive problem. A paper says a system achieved a result. The result is measured on a benchmark. The benchmark is sometimes public, sometimes not. The system is almost never public. Replication depends on whether other teams can reproduce the setup, and frequently they cannot.

This release does not solve that problem. It changes the texture of it. The ten results arrived with executable artifacts. You do not have to trust OpenAI's word that a proof is valid. You can run lake build and watch the compiler work. If the formal statement does not match the mathematical claim, a mathematician can point to the exact line in the Lean file where the translation diverges. If the proof depends on a nonstandard axiom, the axiom list is right there in formalization.yaml.

This is what makes the repository more consequential than the model announcement. Models come and go. A proof object with a build command is a permanent artifact. It will compile the same way in five years as it does today, or it will not, and either outcome is informative.

What is still unknown

The repository answers one question decisively: are the formal derivations valid? If they build, they are.

It leaves several others open. Have working mathematicians independently verified that the formal statements match the intended claims? Do the proofs contain ideas that a specialist would find surprising, or are they formalizations of approaches that were already in the literature? How large was the set of attempted problems, and what was the success rate? What was the specific human contribution at each stage?

OpenAI's announcement page and the accompanying paper address some of these questions partially. The mathematical community will address the rest over the coming months, the way it always does: slowly, through seminars, preprints, and careful reading.

A practical note

If you want to check the proofs yourself, the process is documented in the README. Install Lean 4.32.0 and Lake. Clone the repository. Run lake exe cache get to pull the mathlib oleans, which saves you from compiling the entire mathlib dependency tree. Then run lake build All. The build will either succeed or produce errors. There is no intermediate state where you need to take someone's word for it.

The formalization.yaml file lists propext, Classical.choice, and Quot.sound as the only axioms. Those are the standard three that ship with Lean's core library. If you want to check that no snuck-in axioms are hiding in the proofs, #print axioms on each theorem will tell you.

The repository is at github.com/openai/ten-proofs. The paper is at cdn.openai.com/pdf/ten-proofs-oai.pdf. The reasoning walkthroughs are at cdn.openai.com/pdf/reasoning-walkthroughs.pdf. Sébastien Bubeck's announcement is here. Noam Brown's post is here.

The ComparatorChallenges/ directory contains configuration files for each module. Pick a result, open the corresponding file, and the checking problem is specified.