Ten results, ten different mathematical questions
A research release spanning geometry, groups, codes, and complexity.
OpenAI · Astra research team · mathematical communities
Start with the question
The problem
These are separate research questions: how densely spheres pack, how large error-correcting codes can be, whether every group is sofic, and how difficult certain computations are, among others.
01
From an evaluation to a research collection
OpenAI attributes the arguments to an internal Astra model, with humans preparing manuscripts using the model and subsequent Lean formalizations. Its announcement presents the results as invitations for mathematical engagement. A shared release date should not be mistaken for a shared level of independent review. [1]
02
What is inside
The release covers sphere packing; binary and spherical codes; non-sofic groups; Connes rigidity; arithmetic circuits for the permanent; quantum parallel repetition; closest-vector approximation; Ehrhart’s volume conjecture; multicolor triangle Ramsey numbers; and compactness and degeneracy conjectures in extremal graph theory. [1][2]
03
Read one theorem at a time
The repository gives each result a named Lean module and provides comparator challenges. Its README distinguishes improved bounds from counterexamples and constructions. That map lets readers choose a subject, inspect the precise statement, and compare it with the manuscript instead of treating “ten proofs” as a verification status. [2]
Inspect the evidence
The Lean formalization
Ten public Lean modules and comparator challenges
The repository pins Lean 4.32.0 and supports building All or an individual module such as SpherePacking. Follow its own pinned instructions. We have inspected the repository documentation, not independently compiled or reviewed all ten arguments.
Open the Lean project ↗Sources & further reading
Reviewed 9 Sept 2026. X permalinks were recovered from indexed posts and linked discussions; direct X pages were not consistently accessible. They document the conversation, not proof correctness.
- 1.
- 2.
- 3.
- 4.Levent Alpöge’s response to the release ↗
Public reaction linked for context; the mathematical claims should be assessed from the manuscripts and formal statements.