AWS Builder Center

Builder Center

OpenAI’s 722 Math Papers: AI Enters Discovery

OpenAI’s 722 Math Papers: AI Enters Discovery

OpenAI released 722 AI-generated math manuscripts. Explore how Lean verification, AI reasoning, and formal methods could reshape mathematical discovery.

Rishabh Kankariya

Cloud Computing Student | AWS Enthusiast | Exploring Cloud, DevOps & AI

OpenAI’s 722 Math Papers: AI Enters Mathematical Discovery

Introduction

AI research is entering a phase where the question is no longer simply:
Can an AI solve a difficult mathematical problem?
The more interesting question is:
Can AI generate new mathematical knowledge that humans can verify, understand, extend, and build upon?
On October 6, 2026, OpenAI released a large collection of mathematical research produced by an internal frontier model.
The release contains 722 mathematical manuscripts organized into 372 result families, with supporting proof artifacts and Lean formalizations for many of the results. OpenAI says the evaluation behind the collection involved approximately 4,000 mathematical problems, and that the average result used compute equivalent to roughly three hours of ChatGPT Pro thinking with the internal model.
This is not simply another AI model announcement.
It represents a potentially important shift:
1
2
3
4
5
6
7
8
9
AI as a tool for answering questions
↓
AI as a tool for solving problems
↓
AI as a tool for generating hypotheses
↓
AI as a tool for producing mathematical results
↓
AI-assisted scientific discovery
But there is an equally important distinction:
Generated mathematics is not automatically verified mathematics.
That is where formal proof systems such as Lean become extremely important.

What Did OpenAI Actually Release?

OpenAI published the collection in the public openai/math GitHub repository.
The repository currently contains:
  • 722 manuscripts
  • 372 related result families
  • Supporting proof artifacts
  • Lean formalizations for many results
  • A catalogue of formalizations
  • Manuscript source files
  • Research summaries
  • Information about the evaluation process
  • Revision and citation information
A result family groups related mathematical work together. A family can contain a main result, supporting arguments, consequences, or alternative proofs.
This distinction matters.
The headline number is:
722 manuscripts
But that does not mean:
722 completely independent mathematical breakthroughs.
The 372 families provide a better picture of how the results are related.
OpenAI says the work spans multiple areas of mathematics, including topics represented in pure mathematics, theoretical computer science, and mathematical physics. The repository's reasoning summaries include subjects such as multiplicative functions, the irrationality exponent of π, NP-hardness, arithmetic progressions, spin glasses, free group factors, and relativistic Vlasov–Maxwell systems.

How Were These Results Produced?

According to OpenAI, the collection came primarily from an evaluation of an unreleased internal frontier model.
The model was presented with approximately:
4,000 mathematical problems
The resulting work was then filtered and organized into research families and manuscripts.
OpenAI reports that the average surviving result used compute equivalent to approximately:
Three hours of ChatGPT Pro thinking
with the internal model.
The important point is that this was not simply:
1
2
3
Prompt
↓
One answer
The research process is closer to:
1
2
3
4
5
6
7
8
9
10
11
12
13
Mathematical problem
↓
AI reasoning
↓
Candidate solution
↓
Research result
↓
Manuscript
↓
Formalization / verification
↓
Human mathematical review
This resembles a research pipeline more than a conventional chatbot interaction.

Why This Is Different From Normal LLM Usage

A conventional LLM interaction might look like:
1
2
3
4
5
6
7
User:
Solve this equation.

↓

LLM:
Here is the answer.
The user evaluates whether the response appears correct.
Mathematical research has a much higher standard.
Suppose an AI produces a 40-page proof.
The question isn't:
"Does this sound mathematically convincing?"
The question is:
"Does the proof actually follow from the stated assumptions?"
A language model can generate an extremely convincing argument while making a subtle logical mistake.
That is why mathematical AI needs something beyond language generation.
It needs verification.

The Difference Between Generation and Verification

This is one of the most important concepts in AI-assisted mathematics.
Imagine an AI produces:
1
2
3
4
5
6
7
8
9
10
Theorem:
P is true.

Proof:
Step 1
Step 2
Step 3
...
Step 47
Therefore P.
A human might inspect the proof and believe it is correct.
But another possibility exists:
1
Step 31 contains an invalid assumption.
The final conclusion may still sound convincing.
A formal proof system approaches the problem differently.
Instead of asking:
"Does this proof look correct?"
it asks:
"Can a formal proof checker verify every logical step?"
That is where Lean enters the picture.

What Is Lean?

Lean is a programming language and theorem prover used to formally express mathematical statements and proofs.
Instead of writing only natural-language mathematics:
1
2
3
Assume x > 0.
Therefore...
Hence...
a mathematician can encode the statement and proof in a formal language that a computer can check.
The basic idea is:
1
2
3
4
5
6
7
8
9
10
11
Human / AI
↓
Formal mathematical statement
↓
Formal proof
↓
Lean
↓
Proof checker
↓
Accepted / Rejected
OpenAI says many of the proofs in its new collection have been formalized in Lean and that it plans to add more formalizations over time.
This changes the role of AI.
AI does not have to be the final authority.
Instead:
1
2
3
4
5
AI proposes
↓
Formal system checks
↓
Human interprets
That is a much more powerful architecture.

Why Formal Verification Matters

Consider two AI-generated mathematical results.

Result A

1
2
3
4
5
AI generates proof
↓
Human reads proof
↓
Looks correct

Result B

1
2
3
4
5
6
7
AI generates proof
↓
Lean formalization
↓
Computer checks proof
↓
Proof accepted
Result B provides a stronger form of machine-checkable evidence.
This doesn't mean that formalization makes every mathematical claim automatically meaningful or important.
A proof can be formally correct while proving something uninteresting.
But formal verification addresses a critical question:
Is the stated logical argument valid within the formal system?
That distinction is crucial for AI-generated mathematics.

722 Does Not Mean 722 Verified Breakthroughs

This is where the headline needs careful interpretation.
OpenAI's own repository explicitly states:
The collection contains results at different stages of verification.
Not every manuscript currently has an accompanying Lean formalization.
OpenAI also acknowledges that some unformalized results could contain issues and says it will continue adding formalizations.
Therefore, the correct interpretation is:
1
2
3
722 manuscripts
≠
722 fully machine-verified theorems
Instead:
1
2
3
4
5
6
7
8
9
722 manuscripts
↓
Different verification stages
↓
Some with Lean formalizations
↓
Some still requiring additional verification
↓
Further mathematical review
This distinction is extremely important when discussing AI-generated scientific research.

Why This Could Change Mathematical Research

Traditional mathematical research has a bottleneck:
1
2
3
4
5
6
7
8
9
10
11
Problem
↓
Human researcher
↓
Idea
↓
Proof
↓
Paper
↓
Peer review
The human researcher has to generate the ideas, explore possibilities, construct proofs, write them down, and communicate the result.
AI introduces another research engine:
1
2
3
4
5
6
7
8
9
10
11
12
13
Problem
↓
AI exploration
↓
Thousands of candidate approaches
↓
Promising result
↓
Formal verification
↓
Human researcher
↓
New mathematics
The AI can potentially explore a much larger search space than a human researcher could manually examine.
This is one of the reasons the development is so significant.
The goal isn't necessarily:
Replace mathematicians.
A more interesting possibility is:
Increase the amount of mathematical exploration that mathematicians can perform.

AI Could Become a Mathematical Search Engine

Think about how Google changed information retrieval.
Before search engines:
1
2
3
4
5
6
7
Human
↓
Books
↓
Libraries
↓
Manual research
Search engines changed this:
1
2
3
4
5
6
7
Question
↓
Search
↓
Millions of candidates
↓
Relevant information
AI could eventually do something similar for mathematical reasoning:
1
2
3
4
5
6
7
8
9
10
11
12
13
Mathematical question
↓
AI exploration
↓
Millions of possible approaches
↓
Promising conjecture
↓
Proof attempt
↓
Formal verification
↓
New result
This would turn AI into something closer to a mathematical exploration engine.

From LLMs to Scientific Reasoning Systems

This development also reveals a larger transition in AI.
The original generative-AI paradigm focused heavily on:
1
Text → Text
Then came:
1
2
3
4
Text → Code
Image → Text
Audio → Text
Text → Image
Now another paradigm is becoming increasingly important:
1
2
3
4
5
6
7
8
9
10
11
Problem
↓
Reasoning
↓
Hypothesis
↓
Experiment
↓
Verification
↓
Discovery
Mathematics is particularly suitable for this because mathematical statements can often be represented in formal systems.
That means AI-generated mathematics can be connected to a deterministic verification layer.

The AI + Formal Methods Combination

This is where the technology becomes especially interesting from a computer-science perspective.
You can think of the system as having two major components:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
┌─────────────────────────────┐
│ AI REASONER │
│ │
│ Generate ideas │
│ Explore approaches │
│ Construct candidate proofs │
└──────────────┬──────────────┘
│
▼
┌─────────────────────────────┐
│ FORMAL VERIFIER │
│ │
│ Check definitions │
│ Check logical steps │
│ Check assumptions │
│ Verify proof │
└──────────────┬──────────────┘
│
▼
Verified result
The AI provides search and creativity.
The formal system provides mechanical verification.
This combination could become much more powerful than either component by itself.

Why This Matters Beyond Mathematics

At first glance, this sounds like a mathematics story.
It isn't.
The underlying architecture has implications for many areas of computer science.

1. Automated theorem proving

AI can generate candidate proofs while theorem provers verify them.
1
2
3
4
5
6
7
AI
↓
Proof candidate
↓
Lean
↓
Verified proof
This could accelerate formal mathematics and software verification.

2. Software verification

The same basic idea can apply to software.
Instead of:
1
2
3
4
5
AI generates code
↓
Run tests
↓
Hope everything works
we can move toward:
1
2
3
4
5
6
7
AI generates code
↓
Formal specification
↓
Formal verification
↓
Verified implementation
This is particularly important for:
  • Operating systems
  • Cryptography
  • Security software
  • Distributed systems
  • Financial systems
  • Safety-critical software

3. Cryptography

Cryptographic systems depend heavily on mathematics.
AI could potentially assist with:
  • Finding mathematical structures
  • Exploring conjectures
  • Searching for attacks
  • Constructing proofs
  • Formal verification
The combination of AI search and formal verification could therefore become useful in cryptographic research.

4. Algorithms

AI-generated mathematical insights could potentially help discover:
  • Better algorithms
  • New complexity bounds
  • Optimization methods
  • Graph algorithms
  • Approximation techniques
The important part is that these results can potentially be formally checked.

5. Optimization

Many real-world systems are optimization problems.
Examples include:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Cloud infrastructure
↓
Resource allocation

Networks
↓
Routing optimization

Machine learning
↓
Parameter optimization

Logistics
↓
Route optimization

Finance
↓
Portfolio optimization
Mathematical discovery can therefore eventually influence practical engineering systems.

6. Physics

Mathematical physics is another important area.
The OpenAI repository includes research families involving mathematical physics, including work around the relativistic Vlasov–Maxwell system.
The broader possibility is:
1
2
3
4
5
6
7
8
9
10
11
Physical problem
↓
Mathematical formulation
↓
AI exploration
↓
Candidate theorem
↓
Formal verification
↓
Scientific investigation
AI could become a research assistant for theoretical science.

The Riemann Hypothesis Connection

One particularly interesting area in the release involves the Riemann zeta function.
The repository identifies work concerning a zero-free region for the Riemann zeta function. OpenAI notes that this was one of the exceptions to the standard procedure used for most of the collection, along with work concerning the Hodge Conjecture for CM abelian varieties.
This matters because the Riemann Hypothesis is one of the most famous open problems in mathematics.
However, it is important not to turn every AI result related to the Riemann zeta function into:
"AI solved the Riemann Hypothesis."
That would be an overstatement.
The existence of a result concerning the zeta function is not equivalent to proving the full Riemann Hypothesis.
This is exactly why careful verification and mathematical interpretation matter.

The Human Still Matters

There is an important misconception that this kind of research means:
AI solved mathematics and humans are no longer needed.
The reality is much more complicated.
Mathematical research contains several layers:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Problem selection
↓
Conjecture
↓
Exploration
↓
Proof
↓
Verification
↓
Interpretation
↓
Importance
↓
Communication
AI can increasingly participate in several of these stages.
But a mathematically useful discovery requires more than producing a proof.
Researchers need to understand:
  • Why the result matters
  • How it connects to previous work
  • What it enables
  • Whether the assumptions are meaningful
  • Whether the result can be generalized
  • What new questions it creates
That's where human mathematical expertise remains extremely valuable.

The Publication Problem

The release also raises an important question:
How should AI-generated mathematical discoveries be published?
OpenAI says it consulted its independent Advisory Group on Mathematics and Artificial Intelligence and used its recommendations to inform the release process. It has also established protocols for revisions and citations and says it intends to improve mathematical exposition, citations and presentation in future releases.
The issue is important because traditional research publication assumes:
1
2
3
4
5
6
7
Human researcher
↓
Paper
↓
Peer review
↓
Publication
AI-generated research could produce:
1
2
3
4
5
6
7
8
9
10
11
AI
↓
Thousands of candidate results
↓
Hundreds of manuscripts
↓
Formal proofs
↓
Human review
↓
Research community
That dramatically changes the scale of scientific output.
The research community therefore needs new methods for:
  • Attribution
  • Citation
  • Verification
  • Reproducibility
  • Peer review
  • Versioning
  • AI disclosure
OpenAI's repository attempts to address some of these through version history, citation information and supporting artifacts.

The Verification Bottleneck

There is an interesting paradox here.
AI can potentially generate mathematical results extremely quickly.
But verifying and understanding them can still take humans significant time.
So the bottleneck could shift from:
1
Generating mathematics
to:
1
Understanding and validating mathematics
Consider:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Human researchers
│
▼
Traditional discovery
│
│
▼
AI accelerates discovery
│
▼
Thousands of candidate results
│
▼
Verification bottleneck
│
▼
Formal methods + human experts
This means the future of mathematical AI may not be determined solely by better models.
It may depend equally on better verification infrastructure.

AI + Lean Could Become a New Development Pattern

There is a broader software-engineering lesson here.
Instead of trusting an AI output directly:
1
2
3
4
5
AI
↓
Output
↓
Production
we can create:
1
2
3
4
5
6
7
8
9
AI
↓
Candidate output
↓
Deterministic verifier
↓
Accepted / rejected
↓
Production
This pattern can be applied beyond mathematics.
For example:

Code

1
2
3
4
5
6
7
8
9
AI-generated code
↓
Tests
↓
Static analysis
↓
Formal verification
↓
Deployment

Infrastructure

1
2
3
4
5
6
7
8
9
AI-generated Terraform
↓
Policy checks
↓
Security scanning
↓
Plan validation
↓
Deployment

Mathematics

1
2
3
4
5
6
7
AI-generated proof
↓
Lean
↓
Formal verification
↓
Accepted theorem
This is an important design principle for trustworthy AI systems:
Let AI generate; let deterministic systems verify wherever possible.

What This Could Mean for AI Agents

This research also connects directly to the broader evolution of AI agents.
An autonomous agent needs to make decisions and execute actions.
The dangerous architecture is:
1
2
3
4
5
AI
↓
Decision
↓
Action
A more reliable architecture is:
1
2
3
4
5
6
7
AI
↓
Candidate decision
↓
Policy / verifier
↓
Approved action
Mathematics provides an unusually clean example of this idea.
The AI proposes the proof.
Lean checks it.
The proof checker doesn't care whether the AI is OpenAI, Google, Anthropic or a student writing a theorem.
It checks whether the formal proof satisfies the rules.
That separation between generation and verification could become a major design principle for future AI systems.

What Happens Next?

The immediate future is unlikely to be:
"AI replaces mathematicians."
A more realistic progression is:
1
2
3
4
5
6
7
8
9
10
11
AI-assisted mathematics
↓
AI-generated conjectures
↓
AI-generated proofs
↓
Formal verification
↓
Human mathematical review
↓
AI-assisted discovery
Over time, AI systems could potentially become capable of exploring mathematical spaces that are too large for individual researchers to investigate manually.
The biggest breakthrough may therefore not be one specific theorem.
It could be the development of a new scientific workflow.

The Bigger Picture

The 722-manuscript release is important because it demonstrates a possible transition in the role of AI.
The old model was:
1
2
3
Human asks
↓
AI answers
The emerging model is:
1
2
3
4
5
6
7
8
9
10
11
Human defines a problem
↓
AI explores
↓
AI generates candidate discoveries
↓
Formal systems verify
↓
Humans interpret
↓
Science advances
That is a much more ambitious role for AI.
And mathematics is an unusually good proving ground because formal systems can provide something that many other scientific disciplines cannot easily provide:
machine-checkable correctness at the level of formal proofs.
The 722 manuscripts should therefore not simply be viewed as a collection of AI-generated papers.
They are an experiment in what happens when a frontier AI system is placed inside a scientific discovery pipeline.
The most important question isn't:
"How many mathematical papers can AI generate?"
It is:
"How much trustworthy new knowledge can AI help humanity discover?"
That is the much bigger question.

Key Takeaways

  • OpenAI released 722 mathematical manuscripts organized into 372 result families.
  • The evaluation involved approximately 4,000 mathematical problems.
  • OpenAI reports roughly three hours of ChatGPT Pro-equivalent thinking compute per average result.
  • Many results have Lean formalizations, but not all results are currently formally verified.
  • The collection includes work across pure mathematics, theoretical computer science and mathematical physics.
  • The bigger technological shift is from AI-generated answers toward AI-assisted scientific discovery.
  • Formal verification could become the critical layer separating plausible AI output from trustworthy mathematical results.
  • The same generate → verify architecture has potential applications in software engineering, cybersecurity, cryptography, algorithms and scientific computing.

Explore the Release

OpenAI's announcement:
Sharing AI progress in mathematics — OpenAI 
Public research repository:
OpenAI Math — GitHub 
The Verge's coverage:
OpenAI's 722 mathematical manuscripts — The Verge 
# artificial-intelligence# machine-learning# generative-ai
Any opinions in this article are those of the individual author and may not reflect the opinions of AWS.
Enjoyed reading this content? Let the author know!

Your likes, comments, shares, and saves help creators reach more builders.

Loading recommendations

Loading article