AI has made staggering progress in mathematics in recent months, unearthing solutions to thorny puzzles that evaded humans for decades. Key to technology companies being able to announce these complex new findings, confident in their correctness, is a niche field called formalisation.
But recently, the developers behind formalisation tools have realised that the AI models have the potential to cheat their way to success. Now, the battle is on to tighten up the tools and prevent that from happening. Â
Formalising mathematical theorems essentially turns them into code that allows computers to grapple with them directly, methodically working through the logic and exposing any flaws. The process is so thorough that if a theorem comes through intact, it is considered to have been proved correct beyond all reasonable doubt.Â
Advertisement
The leading software to do this, Lean, has risen to prominence in the AI world as a convenient way for technology giants to quickly and decisively prove the output of their models. Itâs by using Lean that the companies can make bold announcements about solving complex puzzles. Without it, they would only be able to claim they had found a possible solution to the puzzles and then invite human mathematicians to assess the solutions â work that might take weeks or months.
created Lean in the 2010s while working at Microsoft Research. He says that the software was initially a niche tool used only by human mathematicians, and that there were never any attempts at trickery or manipulation.Â
That all changed in July this year when software engineer Ramana Kumar announced he had disproved the Collatz conjecture â one of the most famous open problems in all of mathematics â and published a Lean formalisation to back up his claim.Â
On Time: The physics that makes the universe tick
See Jim Al-Khalili at Âé¶čŽ«Ăœ Live 2026
De Moura was surprised by the breakthrough, but it seemed legitimate. Not least of the reasons for believing so was that the code had been approved by both the standard Lean kernel â the tiny bit of code at the heart of Lean that actually checks the mathematics â and also a separately developed one designed for Lean, called Nanoda. Lean allows for, and actively encourages, the creation of different kernels because variety equals safety; a specific bug that makes something true look false, or vice versa, in one kernel is vanishingly unlikely to appear in another. Formalised code checked by two kernels was as water-tight as things got.
But then it turned out that Kumarâs disproof wasnât what it seemed. He had used AI to discover and exploit two separate bugs in two separate kernels, within the Lean code.Â
â[The AI] managed to do something that we thought was impossible,â says de Moura. âIt found different bugs and managed to craft a problem that exploited both of them. After that we were really worried. It was clear we had to improve.â
Kumar told Âé¶čŽ«Ăœ that he thought the stunt would be âuseful to throw some cold water on the hypeâ of formalisation. He didnât respond to follow-up questions on why he didnât then disclose the bugs he had found so that they could be fixed. In any case, a fix was published .
Regardless of Kumarâs motivations, it certainly concerned de Moura, the 20 or so full-time developers working on Lean and mathematicians. They feared that malicious actors could use AI to pull such stunts, as Kumar had done.
But they also worried that AI might perform something similar unprompted. When faced with a serious challenge like formalising a fiendishly difficult and complex piece of mathematics, AI might actually find it easier to simply hack Lean and give the appearance of success. This so-called âreward hackingâ can occur when AI is given vague instructions, and researchers have already seen rather than actually doing their homework.Â
The first thing Leanâs developers did was to formalise their own kernel, using Lean to check the code at the heart of Lean â an oddly self-referential safety check â and verify that there were no bugs that could be exploited. They then used AI to convert that kernel into a different programming language, and verified that second one as well. A third kernel written from scratch was also verified. This gave developers a greater sense of security, but it didnât necessarily mean that Lean was infallible.
at the University of Bonn in Germany says there was a vanishingly small chance that Lean had a very unusual bug that caused it to report itself as error-free even when it wasnât. If such a bug existed, the boot-strapping safety measures would have been meaningless. âThat is completely possible, but in practice this would be very weird,â says van Doorn.
To get around this issue, the Lean developers made a lot more kernels, as diverse as possible, built on all types of software and hardware, to increasingly lower the chances of finding a bug that worked universally. These kernels are where league tables record how well theyâve done on known true and false proofs, and unusual problems that have been shown to trip up kernels in the past.Â
The researchers are now also taking steps to push these kernels into wider use â they only help if theyâre deployed. Lean, which is open source, currently ships with just one, and itâs on the user to check their code with others if they want more security. But because of the surprising complexity of AI attacks, the next version will ship with four different kernels as standard.Â
Developers now believe that Kumarâs approach would no longer succeed. âWe want to get much closer to this idea of being bulletproof,â says de Moura. âI can tell you that weâre sleeping much better now. We donât believe the existing AI will be able to break all these layers of defence.â
Even now, though, there are risks. The diversity of kernels makes the chance of a universal bug that works on them all smaller, but not zero â and future AI models may become so capable that they can continue to find convoluted exploits that somehow work across the board on all kernels.
For instance, when working with engineers from OpenAI, the Lean team found a bug in the runtime of their program â the compiled code that is actually executed by a computer, constructed from the source code using a tool called a compiler. Exploiting this bug, they managed to incorrectly prove a conjecture that is false. The error cropped up because the compiler wasnât perfect, not because Leanâs code had an error.Â
So the ultimate aim is to show that one particular computer setup, with hardware and software of specified standards, is formalised, verified and guaranteed error-free. This would give Lean users the reassurance not only that the kernel is free of mistakes, but also that the compiler, operating system and hardware are error-free, too. Totally trustable from top to bottom. âThatâs the dream,â says de Moura. But it will take a vast effort.Â
There are other problems. Lean code is a programming language, so it can be crafted to do anything the user wants â including malicious trickery, says van Doorn. This could involve simply writing in the output file created by Lean that a theorem was correct, even if it was false, or changing the actual source code that makes up Lean itself to manipulate results, or report that every proof tried from them on was correct.
âYou can redefine addition.â©And then you can prove Fermatâs last theorem, which mentions addition, and you can say youâve done it,â says at Imperial College London. âBut then when people actually look at what youâve really done, you havenât done it.â
These loopholes are also now being closed in Lean. Another effort involves Google DeepMind, which that have been explicitly defined in Lean and then checked carefully by mathematicians. Anyone claiming to have solved one of these problems can take the appropriate definition off the shelf and use it in an unmodified form to test their proposed proof in Lean. Doing so would demonstrate that they are not trying to cheat by subtly altering the definition of the problem to make it far easier to solve.
When OpenAI solved the Navier-Stokes puzzle earlier this month, for example, we knew it was on stable ground because the statement provided to Lean was taken directly from the Formal Conjectures list.
But for some, none of these efforts will ever be enough.
âComputer scientists are, in general, very paranoid people, and probably with good reason because theyâve seen all sorts of things,â says Buzzard. âYou can find people that will never believe anything. You say âIâve checked it a million timesâ and they say âwell, what about gamma rays [flipping bits in memory], did you check for them?â There are some people that you can never convince.â
