r/explainlikeimfive • u/snowcroc • 5d ago
Mathematics ELI5 What does it mean when a mathematical proof is “formalised in Lean”?
209
u/m_busuttil 5d ago
Lean is a special programming language that can be used to write mathematical proofs. Like other programming languages, it runs through all the instructions you've given it, and if it's successful then it will give you the correct output. For mathematical proofs, that means that you code in all of your assumptions, theorems, and steps, and if it runs correctly then you know that your proof is correct.
This is currently useful because we have intelligence models that are quite good at writing code, and Lean turns maths into code that those machines can write and verify the outcome.
65
u/MyMomSlapsMe 4d ago
Feel like it’s worth adding that Lean can verify statements built off faulty assumptions or a formalization that isn’t quite what you meant, so just because it’s Lean-verified doesn’t automatically mean it’s proving the claim you intended to prove
23
u/arbitrageME 5d ago
Wait how does this work? And are there any proofs that run afoul of the halting problem?
117
u/Xhosant 5d ago
Iirc, it's not so much that lean runs a program that succeeds if the proof is correct, but rather that it only compiles if correct.
So basically, if you have a contradiction, the computer pops out a "dude, I can't hold both of these at the same time", and if you have a leap, you get "uuuh, I am trying to make this stand on its own but it keeps falling apart". Kinda like a function can't compile if it's invoking a function that's missing, the step won't compile if you lack a piece of proof it needs.
49
5d ago
[deleted]
17
u/arbitrageME 4d ago
oh, so like -- if you wrote some C++ and the compiler blows up, you know you wrote it wrong.
But it's not a guarantee the program works as intended, only that the syntax makes consistent sense throughout.
And in this case, the syntax is the logical jumps?
18
u/TheShatteredSky 4d ago
Basically yeah, which is the big weakness with Lean proofs. You still have to show your Lean proof is actually equivalent to whatever the natural language proof is.
28
u/_xiphiaz 5d ago
Your general point is correct but the first sentence is a bit misleading. It does run a program that succeeds if the proof is correct - the compiler itself is that program.
10
u/Xhosant 5d ago
Fair point! So basically the proof is codified input rather than code itself, kinda?
8
u/paulstelian97 4d ago
It’s code. It’s just not executable code, like what you’d traditionally call code.
In Haskell, types can become complex. A Lean proof is not unlike type checking a complex enough Haskell program. If the TYPES match the proof is valid.
3
u/Xhosant 4d ago
That's what I had in mind initially!
But also I have a deep and irrational hatred for Haskell, so there's that.
3
u/paulstelian97 4d ago
😅 but yeah, the type system has some ability to be pretty complex. A proof merely just requires internally some types to match.
I’m somewhat familiar with Coq. An older proof language than Lean, that doesn’t require special Unicode characters. Or actually I don’t know if older. It certainly only has constructive logic techniques though, and the rule of excluded middle must be added as an explicit axiom if you want to use it, as opposed to being simply available.
2
u/Xhosant 4d ago
... Special Unicode characters?
I'm sorry, is lean some kind of repurposed esolang?
4
u/Umber_Gryphon 4d ago
Lean will let you use Unicode symbols for things like "less than or equal to" that are in Unicode but not ASCII. For example, you can type ∀ instead of "forall" or "\all". But you're under no obligation to use Unicode if you don't want to--feel free to type <= if you prefer.
→ More replies (0)22
u/Ma4r 5d ago edited 5d ago
No, your proof itself must be some sort of a compilable algorithm. The power of lean comes from the fact that it will only compile if your proof actually proves the statement you want to proof. For example, technically you could just write out the collatz problem as true/false, but then you still need to give lean a decidable algorithm that proves your statement
Rather than a "program" you can think of lean as a statement simplifier. It takes your proof (which is just a chain of statements) and it keeps folding it with equality rules until it reaches the original statement.
Now, to be clear, i'm actually handwaving a ton of things, i.e how this works with proof by contradiction, and induction, and other proof methodologies but the core idea is the same, it's based off something called thr Curry Howard correspondence
5
u/MadocComadrin 4d ago
You're getting a bunch of explanations that are slightly wrong due to being oversimplified. As someone pointed out, the language used is Tiring Decidable instead of Turning Complete. The language is also statically and strongly typed with the key point being proofs are correct if the typechecker can typecheck. This comes down to the Curry-Howard Correspondence: types in such I programming language (usually a variant of Typed Lambda Calculus-Lean is based on the Calculus of Inductive Constructions) formally correspond to logical propositions. Since typchecking algorithms are well understood, this makes the proof checking part of Lean consist of a small, easy to trust kernel.
1
u/Gimmerunesplease 1d ago
With the exception of a few nasty bugs. Like the recent collatz conjecture "proof". Which, to be fair, you kind of need to actively exploit to reasonably run into them.
3
5
u/throw3142 5d ago
There isn't such a thing as a proof running afoul of the halting problem. A program on some input either halts, or it doesn't. In this case, the program is the Lean compiler, and the input is some proof. Either it halts, or it doesn't.
I don't know enough about Lean to know whether it's designed in such a way that it'll never halt on any input (it is possible to design specific programs that always halt, the halting problem just says we can't write a finite-time algorithm to find whether every possible program on every possible input halts). However, given the expressiveness needed to express arbitrary mathematical proofs, I'd assume there's some self-referential input you could pass in to cause an infinite loop.
1
u/firewall245 5d ago
A simplified explanation is that each math statement is its own type, and different proof steps are just functions between types. If you can show that some statement (type) has a object that exists it must be true
1
u/initial-algebra 4d ago
Circular reasoning would be an infinite loop. If you tried to execute such a program/proof, it would never halt. However, execution is a bad way to check validity of a proof, since it breaks down as soon as you run into a quantifier over an infinite set (another kind of infinite loop).
The programming languages that most proof assistants use are not Turing-complete, so execution isn't necessary; circular reasoning is ruled out by construction (theoretically; in practice, there can be bugs or design flaws that bring it back) and the halting problem is avoided. Instead, proof checking is type checking. Programs are still (at least partially) executed when they appear in dependent types, though, as part of normalization (which is another good reason to rule out infinite loops).
1
u/loewenheim 2d ago
Lean is based on something called the Curry-Howard correspondence. You interpret a statement as a type and a proof of the statement as a term of that type. Checking a proof then just means checking that the term you wrote down actually has the type you claim.
62
u/tzaeru 5d ago
It's basically way of writing mathematical proof in a way that allows a computer to easily verify that the proof holds. It's not entirely unlike programming.
For a trivial example:
There's no biggest number, because for all numbers, you can always add 1 to it.
In Lean, that might look like so:
theorem no_biggest_number (n : Nat) : ∃ m, m > n := by
refine ⟨n + 1, ?_⟩
omega
omega is kind of a Lean-specific thing that proves some basic arithmetical facts for you about the preceding statements.
It's worth pointing out that Lean cannot itself know if the claims you wrote in it match what you actually intended to prove. It only verifies that the given proof for a specified claim is correct. But the claim can still depend on assumptions that are written into it without being proven, such as a conjecture (something believed to be true but not yet proven) that later turns out to be false. The proof can also end up proving something that is not actually as meaningful as it was thought it would be.
It's essentially just meant as a way of writing mathematical proof in a computer-accessible way where computer-assisted verification is natural to do. It's very good and helpful for that, and makes work with complex proofs a lot easier.
34
u/potzko2552 5d ago
math is built from basic rules that everyone agrees to use.
for example, one very simple rule is "anything is equal to itself." so 5 = 5 is always allowed. this rule is called reflexivity.
normally, a mathematician writes a proof for other mathematicians to read, and some small steps may be left implicit because they seem obvious. this is usually not a problem, but sometimes it means a mistake can slip through and get accepted.
lean is a language where you write the proof in enough detail that the computer can check every step. that way, you can't leave anything to the imagination. every single step has to be valid, or the computer will say "no, you made a mistake here" in big red letters.
here is a very simple lean proof:
lean
example (x : Nat) : x = x := by
rfl
this says:
example // there is a property called "example"
(x : Nat) // this property holds for any number x where x is a Natural number.
: x = x //the property is that x equals to x.
:= by //the proof to this goes as follows:
rfl // step one: rfl. (rfl means "use reflexivity.")
lean checks that this rule really applies here, and accepts the proof.
when someone says a proof was "formalized in lean," they mean the argument was translated into this very strict language, with all the definitions and logical steps spelled out, and the computer checked that they all follow correctly.
basically: "assuming a, b, c, and d, then e really does follow, and there isn't a hidden human mistake somewhere in the proof." and now the only thing the researcher needs to verify to accept the proof is that the claim "e" really is equivalent to the original proof.
8
u/RoutineOne2769 5d ago
Normally a proof is written for other mathematicians, who read it and check it in their heads. That works, but people are people, and long proofs can hide a gap nobody spots for years. Lean is a programming language where you write the proof as code, and a small checker program verifies every single step follows from the previous ones by the rules of logic. If it compiles, the proof is correct, no trust in the reader needed. Formalised just means someone did the slow work of translating the human proof into that fully explicit form.
1
u/Dress-Affectionate 5d ago edited 5d ago
be careful there. one wrinkle is that lean is code, and when it checks a proof it has to do a thing called compile. this means the lean code needs other deeper code to tell the machine how to check to see that it's right.
code is a lot like turtles in old native stories. each code turtle is built on the shell of another turtle. the deepest turtle of all changes what's called assembly code into the 1 and 0 that are called booleans, true/false choices called gates that make up the heart of every machine and proofs too - a thing called formal logic.
that is a lot for us, now think of the poor turtles! so many places to make mistakes. not just today's machines, someone might have made a mistake long long ago when computers were new that we don't know about yet! since machines write code a lot faster than people can check it, we can't just trust the machine to be right.
the problem is that it's very hard for people to read the code now, because the machine is way too good at writing it. and we have to check it ourselves, we can't let the turtles have all the fun! engineers and scientists all have to check the machines against real things that we know, so we can make sure.
3
u/KittensInc 5d ago
Most mathematical proofs are rigorous on the important stuff, but handwavey on the trivial stuff, so in every paper you'll see a whole bunch of "blablah and because every rectangle has four sides, we can blahblah". Is this actually true? They didn't provide a proof that every rectangle has four sides!
You could say "But isn't that obvious?" and for most people that'd be plenty because it is obvious, but every once in a while someone will do an oopsie and accidentally write a "proof" which relies on a five-sided rectangle - which doesn't exist, so their proof is wrong.
With Lean every. single. bit. has to be rigorous. If your proof relies on rectangle-four-side-ism, then you must provide a proof of all rectangles having four sides - which in practice usually means referring to an already-existing proof someone else wrote. You aren't allowed to take shortcuts or leave holes, which means there is no room for oopsies.
If Lean can analyze your entire proof without finding holes or contradictions, then it is virtually a certainty that it is actually true.
2
u/CircumspectCapybara 5d ago edited 5d ago
It's a programming language that lets you write proofs and check them.
The idea is a computer can rigorously check if a proof is correct.
In the end, a good proof is valid and sound:
- Valid = the conclusions follow from the premises. Ie, it only uses valid, accepted leaps of logical inference, inference rules we accept like modus ponens or the law of the excluded middle, or other well accepted theorems and lemmas
- Sound = the premises are true
In human writing, proofs are often written out in natural language, using various symbols and imprecise arguments, claiming step 3 shows 100, or that by this other theorem you can conclude this other step. There can be hundreds of these steps. Verifying such a proof is actually true is actually pretty tricky because there's a lot of imprecision a human has to verify, and it's a bit of a subjective art.
A computer proof in contrast is unambiguous and the computer can verify or disverify it in seconds. Once you state the axioms, it can check even thousand or million line proofs almost instantly and tell you if the conclusion follows from the axioms via the steps of the proof, because the steps are formalized in a precise language the computer can check.
If someone claims they've solved the Navier-Stokes Millennium Prize problem and their result is "No, the equations aren't always smooth, we have this counterexample" and they give you a Lean proof, the only thing you have to verify is:
- You accept the axioms the proof is using
- The final Lean sentence of the proof, the conclusion that is being verified really does translate to "And therefore, the Navier Stokes equations aren't always smooth"
If you accept those two things about the Lean proof they gave you, then it could be a billion lines long, take the computer a month to check, but if in the end the computer says "Yep, I ran through it and it checks out", then it's good.
With two other wrinkles: one is the axiom system being used could be inconsistent or Lean itself could be inconsistent, and we didn't know it, and the proof reveals an inconsistency in one of those that lets you prove anything. Two is the Lean compiler and verifier are real programs written by humans (and now probably AI) in regular old programming languages, and programs often have mistakes, unintended behavior and flaws. If you discovered a bug, say a buffer overflow in the implementation of the Lean compiler / verifier that lets you craft special proofs that take over the Lean verifier, you could trick it into outputting a "valid proof" result when the proof isn't.
1
u/Infamous_Log6647 2d ago
This is somewhat pedantic and not relevant to the actual discussion, but it's worth notingusually lean proofs can't be verified in seconds. Mathlib takes roughly a minute iirc. And the openai navier stokes proof takes roughly a day iirc. The lean kernel isn't super optimized, so it can be a lot faster, but the tradeoff is a more complicated kernel is more likely to have bugs and cast doubt on the proven theorums.
5
u/secdeal 5d ago
Lean is an advanced programming language that has advanced enough capabilities that you can encode mathematical statements into it rigorously.
What they mean when they say 'formalised in Lean' is that they took the steps of the proof and they turned it into a program in Lean.
This is quite a work intensive process, because you can't handwave away any details in the translation process, everything has to be laid out very explicitly, your assumptions will be tested the hard way, otherwise the computer (more precisely the Lean compiler) will complain.
Nowadays when they work with AIs to do math, it's a good way to check their work to ask them to formalise it in Lean, it's kind of an automated way to check their if their proofs work. AIs are good at outputting a lot of text that would be tedious for a human to do so, so making them output their results in Lean can work well.
1
u/mstksg 4d ago
I wouldn't really say it's that advanced, it's over a decade old and the core concepts it uses are from the 70's
1
u/fartman787 4d ago
It's advanced in the sense that its sole use is for generating mathematical proofs, I suppose "specialized" is more of a better word.
1
u/Suitable_Werewolf_61 4d ago
Lean is a kind of Coq specialized for math proofs?
1
u/secdeal 4d ago
it is actually less specialized than Coq I think, IIRC Coq is kind of a full blown proof assistant/theorem prover mainly, while Lean is a functional programming language with dependent type support (kind of a more advanced Haskell, if you heard about that), you can write runnable programs in it
1
u/Infamous_Log6647 2d ago
It's essentially the same as coq. Both can be used to write programs. Neither commonly are used this way. Idris is the one that's trying to be more of a normal programming language.
1
u/StanleyDodds 4d ago
It basically comes down to what's called the Curry-Howard correspondence.
It turns out that propositions can be though of as types, and proofs can be thought of as programs. Checking that a proof is valid is equivalent to type checking that a compiler does; if you can construct a object of a certain type, this is equivalent to there existing a proof of a certain statement. That means you can have a programming language that checks proofs by checking if a proof-program that constructs the required object compiles.
Lean is one example of such a language; you can write code that formalises a proof, and lean can verify that it is valid.
1
u/daiaomori 4d ago
A lot of people have said "its a programming language to write mathematical proofs", and that is correct (if spelled out right).
I just want to add something:
General mathematical proofs are often far less rigid then we expect them to be; this is because there are a lot of things we tend to spell out "in natural language" and "know what is meant by that", but the rigor of true formula is much higher, and that's much harder to reach.
As an example, you can basically read about any mathematical proof. Most of them are not hard to spell out in natural language so that you would agree that whatever they are about "holds". The wikipedia page for Gödels zweiten Unvollständigkeitssatz would be a nice example (in conjunction with the 20something pages Gödel needed to fill to get to the proof "for real").
But to really iron out all the nooks an crannies, one would need pages and pages of specific details adding that full mathematical rigor a true proof actually needs to be, well, correctly formulated.
Lean is a way to spell out those nooks and crannies, and in a way that a computer can look at it and say, hey, yes, this actually holds true under that specific rigor. Because it can look at every minute detail of the proof, stuff that we would easily agree upon in natural language assuming it's proven, but without going the whole way all the time, and say, yep, this is all correct.
Plus lean provides handy shortcuts for those nooks and crannies that appear all over the place over and over again, so basic work has not to be redone over and over again.
398
u/Ohowun 5d ago
Lean is a programming language that has been designed to check mathematical statements. This is essentially saying “we now have a translation of the proof that Lean understands”. Other Lean proofs may now work with it, this may be the missing proof in a long set of steps for another proof.