OpenAI has released results from its unreleased internal model, Astra, which successfully solved ten significant open problems in mathematics. The solutions were generated by the model and subsequently formalized into Lean certificates by human researchers.
- High-dimensional sphere packing: New upper bounds on sphere-packing density down to the Cohn–Elkies threshold.
- Binary and spherical codes: Exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance.
- Non-sofic groups: A construction establishing the existence of non-sofic groups, addressing a central open question in group theory.
- Connes’s rigidity conjecture: Disproof of a longstanding conjecture that certain groups are uniquely determined by their von Neumann algebras.
- Arithmetic circuit complexity: New lower bounds for computing the permanent using arithmetic circuits and formulas.
- Quantum parallel repetition: An exponential parallel repetition theorem for general two-player quantum games.
- Closest vector problem: Polynomial-factor hardness of approximation for the closest vector problem, related to post-quantum cryptography.
- Ehrhart’s volume conjecture: Determining the maximum possible volume of a convex body whose centroid is its only interior lattice point in every dimension.
- Multicolor Ramsey numbers: A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.
- Extremal number conjectures: Results on compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180.
The release includes the model's narration of its thinking process for each solution, highlighting a substantial jump in scientific reasoning capabilities that may signal a "mathematical proofs overhang" for future models.