OpenAI just dropped solutions to ten long-standing open problems in mathematics and theoretical computer science, all generated by an internal version of Astra, their next major model. The problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics.
This isn't incremental progress. These are problems that "have been open and have seen no progress on the main result for at least a decade, and in most cases much longer." The total token cost to find solutions? Roughly $2,000 at Sol API rates.
But here's the thing: the mathematical community is not universally excited. OpenAI explicitly acknowledges the Leiden Declaration on AI and Mathematics, signed by researchers concerned about AI's impact on their field. The tension is real, and it's worth unpacking.
What actually got solved
The ten results are genuinely impressive in scope. Let me highlight a few that caught my eye:
High-dimensional sphere packing: New upper bounds on sphere-packing density down to the Cohn–Elkies threshold. This is classical geometry that connects to information theory and coding theory.
Binary and spherical codes: Exponentially improved bounds on the maximum size of binary codes at any prescribed minimum distance. If you care about error correction or information theory, this matters.
Non-sofic groups: A construction establishing the existence of non-sofic groups, addressing what OpenAI calls "a central open question in group theory." This is deep abstract algebra.
Connes's rigidity conjecture: A disproof of a longstanding conjecture about von Neumann algebras. Disproofs are often more interesting than proofs—they rewrite the map.
Arithmetic circuit complexity: New lower bounds for computing the permanent using arithmetic circuits and formulas, including an arithmetic-formula lower bound of order n⁴/log n. Complexity theorists care deeply about permanent vs. determinant.
Closest vector problem: Polynomial-factor hardness of approximation for CVP, a foundational lattice question related to post-quantum cryptography. This has real security implications.
Multicolor Ramsey numbers: A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183. Erdős problems are legendary for being simple to state and brutally hard to solve.
These aren't toy problems. They're the kind of questions mathematicians spend careers thinking about.
How it worked
OpenAI's process is worth noting. Astra generated the mathematical arguments. Humans then prepared the arguments into manuscripts using the same model. After that, the model formalized each argument in a Lean certificate, which is now available on GitHub.
The Lean formalization is critical. Lean is a proof assistant that verifies mathematical correctness mechanically. If the proof compiles in Lean, it's correct—no hand-waving, no hidden assumptions. This addresses one of the core concerns about AI-generated math: how do you trust it?
OpenAI also released "a model's narration of its thinking process" for each solution. This is fascinating from a transparency perspective, though I suspect it will be dissected intensely by researchers trying to understand what Astra is actually doing.
The attribution problem
Here's where it gets uncomfortable. OpenAI states directly:
We believe attribution should honestly reflect how a result was produced: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work.
This is the right stance, and it's refreshing to see it stated clearly. But it also raises thorny questions:
- What does authorship mean when the intellectual work is done by a machine?
- Should Astra get co-author credit? Author credit? A footnote?
- If a mathematician uses Astra to check a lemma vs. generate the entire proof, where's the line?
The mathematical community has strong norms around attribution, collaboration, and credit. These norms evolved over centuries of human-to-human collaboration. They don't map cleanly to human-AI collaboration.
The community response
OpenAI acknowledges the tension explicitly. They mention the Leiden Declaration, which represents mathematicians concerned about AI's impact on their field. The declaration argues for human agency, transparency, and careful consideration of how AI changes mathematical practice.
The fact that OpenAI called this out shows they're aware this is contentious. They write:
There are many views as to the role of AI in mathematics, and we have deep respect and understanding for those concerned with its impact.
But respect doesn't resolve the conflict. Some mathematicians worry that:
- AI-generated proofs might be correct but unenlightening—mechanically sound but intellectually empty.
- The practice of mathematics is as much about understanding as proving. A Lean certificate doesn't convey understanding.
- If AI can solve open problems, what happens to the culture of mathematical research? The mentorship? The community?
These aren't Luddite concerns. They're about what mathematics is—not just producing correct arguments, but building human understanding.
What's already happening
OpenAI notes that their earlier AI-generated disproof of the Erdős unit-distance conjecture, shared in May, has already inspired further developments. They cite five subsequent papers:
- Bloom, Sawin, Schildkraut, and Zhelezov on the sum-product conjecture
- Pohoata on split primes and the Elekes-Rónyai problem
- Saha, Xu, and Ye on furthest pair computation
- Goh and Hatami on communication complexity of point-line incidences
- Lee, Pohoata, and Zhu on the Minkowski grid
This is the optimistic case: AI generates a result, humans engage with it, new ideas emerge. The AI acts as a catalyst for human creativity rather than a replacement.
But it only works if the mathematical community chooses to engage. And that choice isn't guaranteed.
The access question
OpenAI announced ChatGPT for Academic Researchers, providing 100,000 scientists and mathematicians with free access to their best models. This is smart positioning—if you're going to disrupt mathematical research, you'd better make the tools widely available.
They write:
As AI systems evolve into more sophisticated research collaborators, ensuring widespread access is fundamental to supporting scientists and mathematicians as they navigate and define the future of their disciplines during this transformative era.
The framing is careful: "research collaborators," not "replacements." "Supporting scientists," not "automating research." Whether that framing holds depends on how the tools get used in practice.
What I'm watching
A few things will determine how this plays out:
Replication and verification: Will other mathematicians engage with these proofs? Will they find new insights in them, or just confirm the Lean certificates are correct?
Impact on research culture: Do grad students still learn to prove theorems from scratch, or do they learn to collaborate with AI? Both? Neither?
The next frontier: These problems were open for a decade or more. What happens when Astra (or its successors) starts solving problems that are only a few years old? Or a few months old?
Attribution norms: How does the community evolve its norms around credit and authorship? This will be messy and contentious.
The truth is, we're at the beginning of a very strange transition. AI systems can now contribute to mathematical research in non-trivial ways. That's exciting. It's also destabilizing.
The mathematical community will define what this means. OpenAI can release proofs, but they can't control how mathematicians choose to respond. The next few years will reveal whether AI becomes a genuine collaborator in mathematics—or just a very expensive proof-checker that nobody really trusts.