🤖 OpenAI’s Astra solves 10 hard math problems

An internal version of OpenAI’s Astra model solved or advanced 10 complex math problems that had stumped researchers for years. These include proving the existence of non-sofic groups, refuting the Connes conjecture, new bounds on sphere packing and codes, and solutions to three Erdős problems.

Astra also made progress in quantum complexity theory, lattice cryptography, geometry, and graph theory. OpenAI estimates the compute cost was about $2000 using the Sol API pricing.

Humans prepared the results for publication and formalized each proof in Lean for machine verification. OpenAI says the mathematical ideas came from the system, while people handled manuscript prep, formalization, and checks.

📊@tech