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
Independent commentary
Challenge
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. An audit of 18 chapter-specific reviews by Mikołaj and Krzysztof Sienicki found no confirmed substantive error in a principal result, but records that a specialist review asks for major revision of Chapter 8's compressed analytic arguments. The Connes rigidity conclusion has independent support: Shuoxing Zhou reached a counterexample concurrently, and Kun and Thom and Fournier-Facio have built further non-sofic groups on the same mechanism. 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. Andreas Thom disputed the framing of the non-sofic-group result in a guest post on Terence Tao's blog on 2026-09-11. He objects that the announcement described a decade without progress while the proof leaned on his and Gabor Kun's 2019 centralizer-rigidity paper, and he asked whether his own private ChatGPT conversations on the same techniques were available during training or solving. OpenAI's reply, that this did not happen, did not address de-identified training data. The dispute is about attribution and disclosure rather than whether the ten proofs check, so neither grade moved.
Independent checks
Shuoxing Zhou (independent concurrent counterexample): Constructed two non-isomorphic ICC property (T) groups with isomorphic group von Neumann algebras, a counterexample to Connes' rigidity conjecture, with GPT-5.6 Sol assistance and independently of OpenAI's work. Corroborates the conclusion, not OpenAI's stronger infinite-family result. · link ↗
Gabor Kun and Andreas Thom: Analyzed the proof mechanism behind the non-sofic group and extended it to new families of non-sofic generalized wreath products and group doubles. · link ↗
Mikołaj Sienicki and Krzysztof Sienicki (audit of the review record): Audited 18 chapter-specific reviews of the ten results with the Lean formalizations and follow-up work: no confirmed substantive error in a principal result remains; a specialist review requests major revision of Chapter 8; subsequent work reuses the Chapter 3 mechanism and confirms that Connes' rigidity conjecture is false. · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
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.
History of this entry
- CheckedRecorded Shuoxing Zhou's concurrent independent counterexample to Connes' rigidity conjecture, Kun and Thom's extension of the non-sofic mechanism, and an audit of the review record that finds no confirmed error in a principal result but a request for major revision of Chapter 8. No grade moved. source ↗
- ChallengedCited Andreas Thom's guest post on Terence Tao's blog, an attribution and data-provenance dispute over the non-sofic-group result. Neither grade moved: the objection is to the framing and to what was disclosed, not to the proofs. source ↗
- 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.
Community discussion
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}
}