A question about AI and proof [mklab.gr]

[mklabgr]

What If AI Proves a Theorem That Nobody Understands?

---

The Question

What if an AI tool generates a lengthy proof that is verified to be correct, but which nobody — not even the humans who prompted the tool — understands?

This possibility raises one of the most interesting questions about the future of mathematics and artificial intelligence: Can we know that a mathematical theorem is true without actually understanding why it is true?

---

A Proof Without Understanding
If an AI-generated proof were translated into a formal mathematical proof and independently checked by a trusted proof assistant, then the theorem could legitimately be regarded as proved.
Every logical inference could be verified mechanically, even if the complete argument were so long, complicated or structurally unusual that no human mathematician could comprehend it as a whole.
In that sense, the situation would resemble existing computer-assisted proofs, such as the proof of the Four Color Theorem, but pushed to a much more extreme level.
The crucial difference would be that mathematicians might no longer understand the central mechanism of the proof at all.

---

Proof Has Two Different Functions
Mathematical proofs traditionally perform at least two important tasks.
1. Verification
A proof establishes that a theorem is logically correct.
In this sense, the conclusion is:

“The theorem is definitely true.”

2. Explanation
A good proof also tells us why the theorem is true.
It may reveal hidden structures, identify important ideas, expose symmetries, connect apparently unrelated areas of mathematics and suggest new conjectures.
In this sense, the conclusion is:

“Here is the mathematical reason why the theorem is true.”

Historically, these two functions have usually appeared together.
AI may separate them.

---

Verified but Opaque Mathematics
This could create a completely new category of mathematical knowledge:

The verified but opaque theorem.

Imagine an AI producing a proof containing millions or even billions of formally valid steps.
Several independent proof-checking systems confirm that every step is correct.
Therefore mathematicians know that the theorem is true.
But nobody understands the argument.
Mathematics could eventually contain databases filled with such results: formally certified theorems whose proofs remain beyond direct human comprehension.
The next mathematical problem would then become something very different:

The computer has proved theorem T.
Now find the mathematics hidden inside the proof.

---

A New Kind of Mathematical Research
Researchers might begin studying machine-generated proofs in order to extract their underlying ideas.
For example, AI systems or human mathematicians could attempt to discover:
• important intermediate lemmas,
• hidden invariants,
• unexpected symmetries,
• new mathematical structures,
• shorter arguments,
• connections with existing theories.
A proof containing a billion formal steps might eventually be compressed into a ten-page human-readable argument.
In such a case, the original machine proof would establish the truth of the theorem, while the shorter human-understandable proof would explain its mathematical meaning.
Finding that explanation could itself become a major research achievement.

---

But Would We Really “Know” the Theorem?
There is also a philosophical problem.
Suppose no human being understands the proof, but several independently developed proof-checking systems verify it.
Can humans really claim to know that the theorem is true?
Probably yes — but the nature of that knowledge would be different.
The chain of trust might look approximately like this:

Code:

Formal mathematical statement ↓ AI-generated formal proof ↓ Independent proof checker ↓ Verified theorem

The important point is that mathematicians would not need to trust the AI itself.
An AI could make mistakes, hallucinate arguments or produce invalid reasoning.
Instead, mathematicians would trust a much smaller and carefully inspected verification system that checks every individual logical step.
Thus the principle would become:

Do not trust the AI's mathematical authority.
Verify its proof.

---

Certainty Versus Understanding
This leads to a deeper question about the purpose of mathematics.
If the main objective of proof is simply certainty, then machine verification may eventually be sufficient.
But mathematics has never been concerned only with knowing whether statements are true.
Mathematicians also want to understand structures, discover patterns and identify the reasons behind mathematical phenomena.
A proof that nobody understands therefore represents only part of the mathematical achievement.
We might eventually distinguish between:

Proving that something is true
and
Understanding why it is true.

AI may become extraordinarily powerful at the first task.
The second may remain one of the central intellectual activities of mathematicians.

---

The Future of Mathematical Proof
Mathematics would probably not end if AI began producing proofs that humans could not understand.
Instead, mathematical research might divide into two complementary activities.
Machines could establish mathematical truth.
Humans — often working together with other AI systems — could search for mathematical understanding.
In some cases, discovering a human-readable explanation of an already verified machine theorem might eventually be considered more important than obtaining the original proof.
The strange future of mathematics may therefore contain situations in which we can say:

“We know that this theorem is true.
We just don't yet understand why.”

And perhaps one of the most important jobs of future mathematicians will be to close exactly that gap.