Ten Advances in Mathematics and Theoretical Computer Science
OpenAI reports ten results on longstanding problems generated by an internal Astra model, prepared into manuscripts with human oversight, and formalized as Lean certificates.
How should independent mathematical review, formal verification, attribution, and priority work when models can generate many research-level claims at low marginal cost?
OpenAI presents results across geometry, coding theory, group theory, operator algebras, circuit and quantum complexity, lattice cryptography, and extremal combinatorics. The company says an internal Astra version generated the mathematical arguments, humans helped prepare the manuscripts, and the model then formalized each argument in Lean.
The reported inference cost to find all ten results was roughly $2,000 at GPT-5.6 Sol API rates. That estimate excludes model development, problem selection, human preparation, formalization infrastructure, and the wider cost of expert review.
Why it matters
Mathematics is an unusually favorable domain for AI research because important claims can sometimes be reduced to machine-checkable proof objects. Formal certificates do not automatically make a result insightful, novel, or easy for the community to absorb, but they create a stronger acceptance gate than model confidence or stylistic plausibility.
ASI relevance
This is evidence for rapid research generation inside a domain with scalable verification. The next bottleneck may be review, attribution, prioritization, and human understanding rather than raw conjecture production. Independent scrutiny of the individual results remains essential.