Ten advances in mathematics and theoretical computer science
An internal Astra found ten results on decade-old open problems, including non-sofic groups, each with a Lean certificate.
Problems span sphere packing, binary and spherical codes, Connes's rigidity conjecture, arithmetic circuit complexity, quantum complexity and lattice cryptography. Search cost about $2,000 at Sol API rates; humans prepared manuscripts and the model formalized proofs in Lean. Results are company-announced.
- Date
- Saturday, 1 August 2026
- Lab
- OpenAI
- Kind
- paper
- Access
- research preview
Figures
| Measure | Value | Measured by |
|---|---|---|
| Compute cost for all solutions | about $2,000 at GPT-5.6 Sol API rates | company |
Lean certificates check the formal statement, not whether the statement matches the intended problem; independent mathematician verification of each result was not found in sources read.
Sources
This record was checked against its sources on 6 October 2026. How we check