OpenAI takes on the mathematics world with Lean: How formal verification becomes the key to AI self-evolution

Add crowdsourced testing promotional copy Add crowdsourced testing promotional copy end Add App-exclusive traffic routing

People have finally realized that Ke Jie is actually a kind of predicament...

Ten years ago it was Go, then it was the programmers' turn, and recently the ones getting bombarded have become the mathematicians.

OpenAI first opened with the Millennium Prize conjectures, then released more than seven hundred manuscripts in one go, turning the mathematics world upside down.

Recently it even went straight after the ETH assumption, taking out a major cornerstone of computer algorithms, and is now squaring off against that most famous conjecture, P=NP.

This is mathematics, the queen of the sciences, where a tiny handful of humanity's highest-IQ people are active.

Shichao poked around, and wouldn't you know it, it may actually be the mathematicians themselves who made the wedding dress.

As everyone knows, mathematics, especially some of the frontier hard problems, is extremely hard to understand even if some big shot proves it; with references scattered every which way, just reviewing the proof itself takes a lot of effort.

Moreover, when mathematicians write proofs, there are often all kinds of omissions and skipped steps in between; sometimes a single phrase like "obviously it follows" can leap straight over a huge chunk of derivation.

Never mind whether it is obvious; it is probably not even certain whether it follows...

So as computer performance became more and more powerful, computer scientists and mathematicians started racking their brains for ways to let machines handle this part of the review work, which would both save effort and specifically cure this kind of "obviously it follows."

The core of this is a mathematical proof system called Lean. This thing is essentially a programming language; it can turn mathematical propositions and proof processes into a form that machines can understand and strictly check, that is, code.

Mathematics already had a rigorous logical system, and now there are even programs for checking proofs. Isn't this just handing over a pillow when you're sleepy?

So if you want to know why AI has set its sights on mathematics, the verification capability provided by tools like Lean is definitely an important piece of the puzzle.

Having said all that, just how awesome is Lean?

Put it this way: as long as you use it correctly, anything that passes this verification can basically be nailed down as having no problems in the proof process.

Because this guy is too strict and shows no mercy at all; when it works, it is a total stickler for detail.

For example, given a+b = 10, prove that b+a = 10.

This is obvious enough, right? Well, no, you have to break out the "obvious" part and tell it why it is obvious.

Converted into Lean code, it looks like this:

theorem demo (a b : Nat)(h : a + b = 10) : b + a = 10:= by calcb + a = a + b := Nat.add_comm b a_ = 10:= h

In this, you first make clear that a and b are both natural numbers, then translate the problem, telling it that the known condition is "a + b = 10" and what needs to be proved is that "b + a" also equals 10.

Next, choose the "calc" tool to start chained derivation, then call the theorem "Nat.add_comm," that is, the commutative law of addition, to prove a+b = b+a.

Only through this whole set can you derive that b+a also equals 10.

In other words, if you want to get the proof to run, you have to honestly translate the mathematical proposition into a formal language it can understand, and then, according to strict logical rules, construct the proof step by step.

Whether you are calling a theorem proved by predecessors or have just cooked up a new conclusion yourself, you have to provide a legitimate logical basis.

Most critically, although Lean is both huge and complex, unfortunately mathematicians are all obsessive-compulsive, so the underlying architecture and logic are top-tier clear.

Inside, proving and checking are split into two separate matters; no matter how complex the preceding proof program is, the final check and decision are made by that short and sharp kernel.

This way, the risk of bugs is greatly reduced, and it is also very convenient for humans to do a second review.

In addition, Lean has a heavyweight teammate called Mathlib, which can be called the open-source arsenal of the mathematics world.

From algebra and calculus to number theory, topology, and so on, countless things studied by predecessors have been translated by mathematicians into a form Lean can understand and stuffed into Mathlib.

Today, this arsenal has accumulated more than two million lines of formalized mathematical content.

In the future, when encountering theorems that predecessors have already proved, there will be no need to derive them from scratch; you can just call them directly from Mathlib.

After going through the materials, Shichao discovered another possibility: that their work in mathematics may really have been something done along the way.

Because Lean's potential goes far beyond this; it can also be tied to the hottest concept in the current AI circle, namely AI self-evolution, RSI.

As everyone knows, in current model training, besides computing power being in tight supply, high-quality data is also a top-tier hot commodity.

Shichao wrote before that this business is almost smoking across the ocean, with shockingly high hourly wages.

How to go about it? Back then, AlphaGo set a good example.

Later, the reason it was able to grind human Go players into the ground depended not only on memorizing game records, but also on playing against itself, that strange trick of left brain versus right brain, and only then did it fully max out the iteration speed.

But the problem is that Go has clear rules; who wins and who loses, and how many points, can be known by the system with one calculation, making it very easy to simulate.

If you take a bunch of poisoned fake data and use it for "self-evolution," then within just a few rounds, GPT will be trained straight into a talking Tom cat.

At this point, looking again at a formal verifier like Lean, isn't it just the chosen one?

It doesn't rely on human experts to grade papers; it can automatically provide basically reliable feedback that can also be scaled up.

With Lean as this cyber perpetual-motion donkey, AI can, like in the Go days, day and night trial and error in the world of mathematics, get feedback, grind experience, and step on its own foot to start super evolution.

Although it won't directly achieve RSI self-evolution, at least it's touching the edge of it.

As for how tempting the prospects are, just look at the moves of the big companies.

Not only is OpenAI attacking hard, the rumors next door at Anthropic are also not small; they've hired a bunch of human mathematicians.

And our Google the great philanthropist, as early as 2024, used Lean to build a system called AlphaProof for experiments, reaching the level of an Olympic math silver medal, and later published a paper in Nature.

In addition, Lean is also very good at treating AI hallucinations.

Lean's founder Leonardo de Moura mentioned a very hardcore example: having AI use Lean to rewrite the underlying zlib compression library.

You may not have heard of zlib, but you only need to know that it is something at the level of internet infrastructure; the images we use, compressed packages, and so on are all related to it.

Engineers had Claude refactor it once using Lean, and conveniently also used mathematical logic to prove this:

"For data within a certain size range, no matter what compression level is used, as long as it goes through this program to compress and then decompress, it can be restored exactly as it was."

This is quite powerful, because it is not testing hundreds of thousands of files one by one, but proving mathematically that as long as these conditions are met, the result will not go wrong.

But now, the review has been replaced by Lean, this unfeeling program, so the conclusion can be considered quite reassuring.

You can't say the entire zlib library will be completely bug-free from now on, but after going through this whole process, the probability of AI making things up is genuinely reduced.

Of course, that said, although Lean's efficacy is awesome, its scope is still quite limited and it can't cure all diseases.

For example, when it does problems, it is strict but rigid; although it can judge whether the intermediate derivation process follows the rules, it doesn't care whether the "problem" you wrote at the beginning was written correctly.

If, when translating a real-world problem into Lean code, you accidentally write the meaning of the problem crookedly, or take a conclusion that originally needs to be proved as a known condition in advance, then as long as you can later make it circle back, Lean will still check it and pass it.

Even more ruthlessly, it completely doesn't care whether what is proved has any value.

AI can completely use a few axioms and permute and combine them into millions of absolutely correct, Lean-checked-and-all-passed boilerplate theorems, but this is meaningless.

It's like a student who already knew how to solve quadratic equations in one variable, and now every day makes up ten thousand more to solve; no matter how high the correct-answer rate is, their math level probably won't undergo any qualitative change.

And in the end, the real world is not something where everything can be neatly stuffed into formal language like mathematics.

Most of the trivial matters in our daily lives, from writing an article that makes everyone laugh to formulating a complex social policy, almost all have difficulty having a unified quantitative standard.

Even "right and wrong" itself is often a relative concept, full of gray areas and the quagmire of interest trade-offs.

A formal verification tool like Lean, which insists on black and white, may not even have a place to set foot.

So after seeing this wave of OpenAI operations, everyone actually doesn't need to be too anxious.

Whether it can get mathematics straight is still undecided; as for the scarier RSI, at present it is only a sign, regarded as a beautiful vision people have for AGI.

It's just like back when the laws of thermodynamics had not yet been figured out, perpetual motion machines also made countless smart people rush forward one after another.

But later physics told us that this thing is fundamentally unworkable.

Of course, RSI is not a perpetual motion machine, nor does it violate any known laws of physics.

As for whether something is valuable at all, whether it is worth doing, and why humans want to do it?

Rest assured, the final right of interpretation of this matter still belongs to us humans.

After all, bipedal upright apes don't care about your input-output ratio; many big jobs done out of sheer boredom are actually just out of sheer boredom...article_adlist[

Responsible editor: Ruofeng

Article content report ]article_adlist Statement: Sina exclusive manuscript, unauthorized reproduction prohibited. tech_web_article_v2015_block_bottom non-targeted 300*250 button 17/09 wenjing begin

non-targeted 300*250 button end