AI Solves Mathematics and AI Verifies It—But Who Ultimately Verifies Lean?

The other day, I saw a report that AI had solved a problem related to the Navier–Stokes equations, one of the difficult areas of mathematics.

The Navier–Stokes equations describe the motion of fluids, and some difficult questions about their mathematical properties remain unsolved. I was surprised that AI had begun venturing even into such territory.

Later, I saw another announcement saying that AI had proved a large number of mathematical propositions.

What caught my attention was not the number of proofs, but how they had been verified.

AI makes mistakes without hesitation. Even if it generates thousands or tens of thousands of complex mathematical proofs, having humans check each one to determine whether it is truly correct would be an enormous task.

Apparently, however, the proofs had been verified using something called Lean.

I had never heard the name before, so I looked it up and found a fascinating system.

AI Develops the Proof, and Lean Verifies It

Lean is a type of software known as a proof assistant, designed to let computers rigorously verify mathematical proofs.

Because AI generates text and equations probabilistically, it can produce plausible-looking mistakes. Lean, by contrast, mechanically checks whether a proof follows formal rules of logic.

In other words, no matter how confidently an AI presents an incorrect proof, it fails unless it passes Lean’s verification.

That is what makes the system interesting.

I had assumed that when AI solved a difficult problem, human mathematicians would ultimately have to spend enormous amounts of time verifying the result.

But if the proof itself can be formalized, its verification can also be entrusted to a computer.

AI constructs the proof, and Lean verifies its logical correctness.

Humans no longer need to trace every equation line by line.

However, Lean guarantees only that a proof is valid for the given assumptions and proposition. Whether the proposition being proved represents the right question in the first place is a separate matter.

Will Programming Follow the Same Path?

When I learned how this worked, software development was the first thing that came to mind.

A development style in which humans review AI-generated code is now becoming widespread.

But human review also has limits. It is impossible to understand every detail of complex logic and discover every defect.

If so, perhaps AI should write the code while another program formally verifies its correctness.

Of course, with ordinary software, defining what counts as “correct” is itself difficult. Even so, it seems natural to let machines take over the parts that can be verified.

AI implements, and a machine verifies.

The human role may shift away from checking small pieces of code and toward deciding what should be built and what standards should define correctness.

Then Who Verifies Lean Itself?

After thinking this far, another question occurred to me.

Lean is, after all, a program too.

If there is a bug in its core proof checker, it could potentially judge an incorrect proof to be correct.

And once AI takes charge of software development, AI will probably also develop and maintain Lean itself.

So who guarantees the correctness of Lean after AI modifies it?

Simple. We build another program to verify Lean.

Then who verifies that program?

We build yet another verification program.

And so, in exchange for being freed from the work of solving difficult mathematical problems, humanity gains a new job: verifying the program that verifies the program that verifies the proof.