OpenAI published ten results in mathematics and theoretical computer science that it says resolve or substantially advance long-standing open problems, generated by an internal version of Astra, described as its next major model. The problems span high-dimensional sphere packing (upper bounds down to the Cohn–Elkies threshold), binary and spherical codes, the existence of non-sofic groups, a disproof of Connes's rigidity conjecture, arithmetic-formula lower bounds of order n^4/log n for the permanent, quantum parallel repetition, hardness of the closest vector problem, Ehrhart's volume conjecture, and Erdős problems 183, 146 and 180. OpenAI states the token cost of finding the solutions would be roughly $2,000 at Sol API rates, that humans prepared the manuscripts, and that the model formalized each argument in Lean certificates released on GitHub.