OpenAI published ten mathematical results produced by the Astra model, along with code for verifying the proofs
OpenAI published ten mathematical results produced by the Astra model, along with code for verifying the proofs
On 1 August, OpenAI presented ten results in mathematics and theoretical computer science, addressing problems on which the main result had not advanced for at least ten years. According to the company, an internal version of the Astra model obtained the results. Human researchers working with the same model prepared the manuscripts, after which Astra expressed each argument in Lean 4, a language for checking formal proofs.
The papers cover several fields, including sphere packing, coding theory, group theory, quantum complexity, lattice-based cryptography, and extremal combinatorics. The results include the construction of a nonsofic group, a counterexample to Connes’ rigidity conjecture, and new lower bounds for computing the permanent, a function of a matrix. The collection does not rely on a single common technique. OpenAI reports results for ten distinct long-standing problems.
The company released the manuscripts, explanations of the reasoning, and a repository containing the formalizations. The repository includes a separate file for each of the ten results and a single command that builds them together. This gives mathematicians two objects to examine: a manuscript presenting the proof idea and a formal version that software can check.
Lean expresses theorems and their proofs in a strict formal language. Its checker either accepts the formal statement and proof or reports an error. The formalization therefore records the exact claim that the authors regard as proved and allows another researcher to run the same check.
The search for an argument has produced more than a statement from the company. It has also produced manuscripts and code. Researchers can examine them side by side, study the mathematical idea in the text, compare it with the formal version, and reuse the recorded lemmas in a later proof.