NederlandsLean
Lean is a programming language and helper program for mathematical proofs. Every definition and every step is written down so precisely that the computer can check whether the proof is correct.
Lean is a programming language in which you write down mathematics so precisely that a computer can check every step. Such a program is called a proof assistant. You write down a theorem and a proof, and Lean checks whether the proof really establishes the theorem, without guessing and without skipping anything.
It is comparable to a teacher who goes through a worked solution line by line and rejects the whole proof as soon as a single step is wrong.
How does it work?
In Lean, definitions, theorems and proofs are written as code. The core of Lean is small and is widely trusted. Everything built on top of it does not need to be trusted separately: Lean checks it. A proof that Lean accepts is therefore correct for what has been written down. It remains important, though, that the definitions in Lean say exactly the same as the mathematics that is meant.
Writing it down takes a lot of time, because you have to spell out every step. AI can help with that. The AI comes up with something and writes it out, and Lean checks it. This checking with mathematical certainty is called formal verification.
Why it matters
Lean is in the news because AI produces mathematics on a scale that no human can check. The company Axiom Math had dozens of AI agents spend 24 days converting the roughly 15,000-page proof of the classification of finite simple groups into Lean code (link). Along the way they found deviations in the published work, which have been repaired.
For new results, too, such a computer check is valuable. OpenAI says its internal AI models have solved three long-open problems in mathematics, computer science and physics, and part of the proofs has already been checked by a verification program (link). Shortly afterwards Anthropic reported that an internal Claude model had itself found a faster way to solve a famous computational puzzle, with a proof that a computer had already checked (link). That way mathematicians do not have to recompute everything themselves to know that it is right.
Articles about Lean
-
PSI: AI found proof of a 2008 conjecture on the limits of quantum computers
The US company Physical Superintelligence says its AI system found a proof of the Aaronson-Ambainis conjecture, an open question from 2008 about when quantum computers are much faster. The program Lean has approved the proof; fellow researchers are now checking it.
-
AI agents turn 7,500 pages of mathematics into proofs that a computer can check
The US company Axiom Math has used AI agents to turn a mathematical reference work of about 7,500 pages into 16 million lines of code that a computer can check. Along the way, the agents found dozens of points that needed refining. People are now continuing to review the work.
-
Ten AI agents deliver a computer-checked proof for a puzzle with seven electrons in fifteen hours
The company Vals AI had ten AI agents write a proof in fifteen hours for a puzzle more than a hundred years old: how seven electrons arrange themselves on a sphere. A computer checked every step. The next step is a review by mathematicians.
-
AI agents turn the longest mathematical proof ever into checkable code in 24 days
The American company Axiom Math had dozens of AI agents turn the proof of 'the enormous theorem' about symmetry, some 15,000 pages, into code a computer can check. Along the way they found 34 deviations in the published work, which have now been repaired.
-
Anthropic: Claude also disproves a conjecture about computing time that is almost thirty years old
Anthropic says an internal Claude model found a faster way to solve a famous computing puzzle on its own. OpenAI reported the same result shortly before, as one of its three AI breakthroughs. A computer has already checked the proof; mathematicians are now looking at whether it holds.
-
Start-up PSI uses AI to help publish five quantum proofs that a computer can check
Physical Superintelligence has used its own AI system to tackle five open questions in quantum information theory. Each proof is also written in Lean, a program that checks proofs step by step. Other researchers can now check them for themselves.
-
What mathematicians think of OpenAI's 372 maths results
In early October, OpenAI put 372 results on open maths questions online. Mathematicians are impressed, but checking them will take months. What has been claimed, and what do experts think?
-
OpenAI: its own AI cracked three major problems, and top scientists will check the work
OpenAI says its internal AI models have solved three long-standing problems in mathematics, computer science and physics. Part of the proofs has already been checked by a verification program. Independent experts will now examine whether everything holds up and what it means.
-
Humanoid robot from South Korea pushes 35 kilos and lifts 20 kilos while walking
Researchers at KAIST in South Korea had their humanoid robot push objects of up to 35 kilos and lift up to 20 kilos while walking. Legs and arms are controlled together by a single AI system. It is a demonstration in the lab; more tests will follow.
-
OpenAI publishes 719 mathematical manuscripts from a not-yet-released AI model
OpenAI has published 719 mathematical manuscripts on GitHub, produced by an unreleased internal model. According to the advisory group AGMAI, they contain solutions to 'hundreds' of open questions. Independent review has yet to begin.
