Ten results in mathematics and theoretical computer science with Lean certificates
An unreleased OpenAI model produced ten results including the first explicit non-sofic group and a disproof of Connes's rigidity conjecture, each published with a machine-checkable Lean 4 proof.
- Lab
- OpenAI
- Model
- Astra
- Field
- Mathematics
- Date
- 2026-08-01
- Problem posed
- 1999 · open 27 yrs
Sources
Original work
Announcement
What was found
The ten cover high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes's rigidity conjecture, arithmetic circuit complexity, quantum parallel repetition, the closest vector problem, Ehrhart's volume conjecture, multicolor Ramsey numbers and extremal number conjectures. Soficity was introduced by Gromov in 1999 and whether a non-sofic group exists had stood open since; Connes posed his rigidity conjecture in 1980, and the disproof constructs infinitely many non-isomorphic property (T) groups sharing a von Neumann algebra. Humans used the same model to prepare the manuscripts and then to formalize each argument in Lean 4.32.0. OpenAI put the token cost of finding all ten at roughly $2,000 at Sol API rates.
Novelty check
Each of the ten is a named open problem with a documented origin: soficity from Gromov 1999, Connes rigidity from 1980, and the sphere-packing exponent improvement is the first on the general bound since 1978. The Lean repository states which prior bound each result improves. Thomas Bloom, who maintains erdosproblems.com and publicly corrected OpenAI's 2025 Erdős retrieval episode, called these results big news, which is meaningful given that he is the person who caught the previous overclaim.
Caveats and known objections
The certificates are checkable and the claim that the theorems hold is as solid as Lean makes it. The claim about provenance is not checkable: Astra is unreleased, so no outside party can test whether the model produces these results, and the account of how they were found rests entirely on OpenAI. Grading verification as formal reflects the proofs, not the provenance; a reader who cares only about who found it should read this as claimed. Specialist review of the mathematical significance is still pending in several cases. Noam Brown noted there are no Millennium Prize problems here. Press summaries of the ten disagree with the repository's own list, some substituting specific Erdős problem numbers that do not appear in it; the list above follows the repository.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Ten results in mathematics and theoretical computer science with Lean certificates. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-01-astra-ten-advancesBibTeX
@misc{whataifound-openai-2026-advances,
title = {Ten results in mathematics and theoretical computer science with Lean certificates},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-08-01-astra-ten-advances}
}