Aug 1, 2026
OpenAI publishes ten results from an internal Astra model, spanning sphere packing, binary and spherical codes, non-sofic groups, Connes’s rigidity conjecture, arithmetic circuits, quantum parallel repetition, closest-vector hardness, Ehrhart’s conjecture, Ramsey numbers and extremal graph conjectures.
The announcement distinguishes resolutions from substantial progress. Humans prepared manuscripts with the model; OpenAI says each argument was formalized in Lean. Links lead to the papers and reasoning walkthroughs.