Dimensionality reduction strike, the math PhD is burning the midnight oil and going bald, AI mathematician: set problems in the morning, submit the proof at 4 p.m.

Since February this year, AxiomProver has made 8 AI papers covering the most hardcore fields appear on arXiv, and 6 more are in preparation. The pace of setting questions in the morning and submitting answers in the afternoon has made the days when doctoral students go bald and professors strive for promotions a thing of the past. What can AI achieve next?

Mathematicians can't sleep!

Imagine you are a reviewer.

One day, a paper lands in your hands. It claims to have proved a problem that has puzzled peers for decades.

You take a deep breath, make a cup of coffee, and start checking line by line - it may take months, or even years.

This is not an exaggeration.

In the mathematical community, it is common for hardcore papers to wait two or three years from submission to publication.

The entire modern mathematics is built on an extremely expensive, extremely slow, and occasionally faulty "human credit system".

Behind every "correct" result, there is a human expert who is exhausted and seeing stars vouching for it.

Now, mathematician Ken Ono says: It's time to upgrade this system.

Ken Ono's words carry a lot of weight. He is called a "legend in the mathematical world" by Ken Ribet, the former president of the American Mathematical Society.

Ken Ono is well - known for his in - depth research on the theories of the Indian mathematical genius Srinivasa Ramanujan. He also leads a top undergraduate research project in the United States and has trained 10 Morgan Prize winners, including Hong Letong, a post - 2000 from Guangzhou, the founder of Axiom.

An AI that can solve difficult problems in one morning

This AI tool is called AxiomProver.

How powerful is it?

It is reported that since February this year, 8 papers have quietly appeared on arXiv (the place where mathematicians around the world post pre - prints), covering the toughest fields such as algebraic geometry, representation theory, number theory, and combinatorics.

Five of them have been accepted by authoritative mathematical journals, several others are under review, and 6 more are in preparation.

As far as they know, it is the first time in history to introduce "papers + formal proof certificates" into journal literature in this way.

But what really makes people's hair stand on end is the speed.

Sometimes, a mathematician throws an unsolved open research problem to the system at 10 a.m. By 4 p.m. the same day, the AI can give a complete, machine - verified proof.

Set questions in the morning and submit answers in the afternoon. There is just time for a lunch in between.

In the past, this would have been a result that could make a doctoral student go bald and a professor get promoted.

Why is it "never wrong in calculation"?

At this point, you may frown and ask: Don't AIs often talk nonsense seriously? Why should we trust this thing?

That's a good question. This is exactly the most crucial part of the whole thing.

Ordinary large language models (the chat AIs you use every day) essentially "guess" the next most likely word.

Guessing too much will naturally lead to mistakes - when they first came out, they couldn't even do elementary arithmetic right and were ridiculed for a while.

But AxiomProver takes a different approach. All the proofs it generates are written in a formal language called Lean.

What is Lean?

You can think of it as an impartial and emotionless machine referee.

It doesn't care how elegant your proof reads or how ingenious your thinking is. It only cares about one thing: whether each step of the reasoning is logically air - tight. If there is a single symbol wrong, sorry, it won't pass.

Therefore, the "correctness" of AxiomProver's proofs no longer depends on a human expert staying up late to check for you, but is stamped and endorsed by the machine on the spot.

It can't get away with mistakes because once it makes a mistake, the machine will know right away.

Human reviewers can get tired, sleepy, and make mistakes. Machine referees won't.

The "credit crisis" and "speed bottleneck" in mathematics are collapsing

Now, we can talk about the real significance of this matter.

Scientific discovery has long been stuck in two persistent problems.

The first is the credit crisis.

Whether a mathematical proof is correct ultimately depends on human judgment. But humans can make mistakes, have biases, and have limited energy. This "human - endorsed" system is inherently fragile.

The second is the speed bottleneck.

Reviewing a paper can take several years, not because reviewers are lazy, but because the speed of human brain calculation is just that slow. No matter how smart a person is, there are only 24 hours in a day.

AxiomProver's approach is like firing a shot at these two pain points at the same time.

Leave the credit issue to the machine: The stamp of the Lean checker is more reliable than any human expert.

This is why journal review can be incredibly fast - reviewers no longer need to check from scratch. They only need to judge whether the result is important and well - written.

Leave the speed issue to computing power: Setting questions in the morning and submitting answers in the afternoon was unthinkable in the human era.

This AI has caused an earthquake in the mathematical community.

In October last year, OpenAI claimed that GPT - 5 "solved" 10 Erdős problems.

The mathematical community called it a fraud. Demis Hassabis said it was "embarrassing".

Seven months later, OpenAI and DeepMind both announced verified mathematical breakthroughs in the same week.

What Axiom wants to do is to push mathematics from the "handicraft workshop" agricultural era into the industrial era of "instant verification and machine endorsement".

What can AI achieve next?

Reference materials:

https://x.com/axiommathai/status/2059640252546126087?s=20https://www.axios.com/2026/05/26/axiom-ai-math-journalhttps://axiommath.ai/papers

This article is from the WeChat official account “New Intelligence Yuan”. Author: ASI Revelation. Editor: David. Republished by 36Kr with permission.