So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
6gvONxR4sf7o 22 hours ago [-]
Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.
thom 16 hours ago [-]
How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.
herni 11 hours ago [-]
I think you misunderstand what a LEAN proof entails.
A statement corresponds to a type and to proof that statement means to show that this type is inhabitetd (i.e., there is actually a value of that type).
A proof is then "just a program" in "just a programming language". Crucially, you do not care what "this program computes" but you care only that the program actually has the given type.
There is no concept of a "bug" in a proof term because you do not actually care what a proof term "computes". You care that it exists and that it is well typed.
thom 10 hours ago [-]
How would you characterise the 4833 issues surfaced by this work?
> inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
thom 12 hours ago [-]
Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless
In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
SkiFire13 4 hours ago [-]
> Surely “the proof is the one you think it is” is the whole ballgame?
No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.
ndriscoll 11 hours ago [-]
Because it won't type check. It's like asking how you know some function in a program really gets an Int argument when you had lots of data structures you were passing around with all kinds of fields with various names and types.
If you construct value of type `forall n, exists m, m≥n and m prime`, then you know you have such an object. Think of a `theorem` (the Lean keyword) as a function that returns such objects. If you try to return the wrong type (e.g. you build a `forall n, exists m, m≤n and m prime`) in your "function" body, you get a compile error. If you use types incorrectly in the middle (passing values and intermediate proofs to theorems incorrectly), you get a compile error.
It's just like any programming language except the type system is rich enough that in addition to being able to have a value x: Int, (so maybe x is 5) you can have values like h: x^2≥0 (so imagine h is some object you build that proves x^2≥0).
thom 10 hours ago [-]
Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:
import Mathlib
abbrev Scalar := ℂ
abbrev Real := Scalar
theorem negative_one_has_a_real_square_root :
∃ x : Real, x * x = -1 := by
exact ⟨Complex.I, Complex.I_mul_I⟩
But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!
ndriscoll 10 hours ago [-]
What people are telling you is you need to check the signature of negative_one_has_a_real_square_root (which includes the definition of Real). Generally this is an easy task. Did you define things the way that you meant to define them to make the statement that you meant to make? Then you can trust that the 500k lines that prove it are fine.
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
thom 9 hours ago [-]
Right but... the difference between "a robot may not injure a human being" and "a robot must injure a human being" is quite important in the real world, even if the "mathematical content is correct". And if my silly example is too contrived, it still seems like this sort of thing happens all the time:
That paper seems to just be saying that people's benchmarks are bad. Like, yeah, obviously don't consider the problem solved if the bot used sorry or axiom. This is trivial to check for and consider a compile error. It's (literally) the same as just not allowing throwing exceptions in a program. And vacuous statements aren't actually a problem. And they claim that sometimes it makes mistakes formalizing an informal statement, but that this becomes noticeable when you try to actually prove it. This is like if it forgot a parameter when it was defining a function prototype. When it actually goes to write the function, it realizes it needed some extra information, so it'll just add it. So, again, what's the problem? This isn't the type of error that can go uncaught because it won't be able to proceed with the actual proof unless it's actually true, in which case, great, it proved a stronger statement than was asked for.
A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.
You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.
After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.
I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.
thom 8 hours ago [-]
So the types of errors in that paper could never lead a mathematician to make a claim about a Lean proof that was later found to be incorrect?
The core of a proof checker is a formally validated core that is based on a small amount of concepts. Every single line in the proof reduces to that core, therefore, as long as you can trust the core, you can trust the execution of the proofs.
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
thom 12 hours ago [-]
Yes but why do we write the last bit as an aside as if that’s not a massive yawning black hole for errors to hide in? All the other stuff is irrelevant, just like when Haskell and Rust people claim that if their code compiles it is correct.
ndriscoll 11 hours ago [-]
Because in practice, it's very straightforward to check that all of the types for class members are what you expect. Especially when you actually use that class in other code. You have things in mind that the class should do. If you get compile errors doing those things, you notice the inconsistency.
ubj 20 hours ago [-]
This. Lean does not remove human responsibility, but it does assist in reducing the surface that the human needs to inspect and verify.
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.
rzmmm 13 hours ago [-]
Well, the statement can be the 500k line part if it's generated with an LLM. But I think some people miss the point of Lean when they use LLM like that.
thaumasiotes 21 hours ago [-]
> but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan?
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
thom 16 hours ago [-]
Hidden like any subtle bug that one might gloss over when inspecting the source code. The statement you’re trying to prove could be thousands of lines long and that semantic mismatch could occur anywhere. We seem to be very blasé about this.
mswphd 15 hours ago [-]
that's misunderstanding what lean does. It proves many statements of the form A implies C (I'll write this as A => C). If you chain many of these together, say A => B1 => B2 => ... => B500_000 => C, what you do is
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).
thom 12 hours ago [-]
Okay this is more revealing, thank you. You’re saying that A and C are very small, humanly verifiable pieces of encoded logic. Can you give me an example of how Bs come into being and why they can never be wrong?
Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.
A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."
dnautics 19 hours ago [-]
There are things you can do in lean which are footguns. For example, 1/0 = 0 in lean. For much of math that's not a problem. Still though, you have to remember that this is the case for whatever number system you're doing a proof in. For things which map to real world scenarios it's potentially a big problem.
thaumasiotes 6 hours ago [-]
> Still though, you have to remember that this is the case for whatever number system you're doing a proof in.
This is generally untrue. The reason you don't have to remember is that your proof will inevitably rely on a theorem with "x ≠ 0" as one of the premises. (And if that doesn't happen, then the fact that lean defines division strangely isn't relevant to your proof.)
If what you're doing is writing code unaccompanied by proofs, then yes, this is something you'd have to remember.
dnautics 3 hours ago [-]
> theorem with "x ≠ 0" as one of the premises
If you're writing that theorem: Assuming you remember to include it in your premises.
Sometimes the invariant might not be mathematical, it might be social. I recall a story where 1/0 caused a problem because stock issuance uses a 0-share disbursement as a tombstone: to indicate that "this stock account has zeroed out this security and has no remaining ownership". You might not have remembered that and you might have forgotten to record that as a necessary invariant in your proofs. If lean had defined division to have a nonzero denominator, it would have caught the problem even if you didn't know that a zero share disbursement hada a different meaning.
OP: Your article shows “[Contents]” where presumably the table of contents is to be displayed.
alexeldeib 21 hours ago [-]
It's a button
WalterGR 20 hours ago [-]
So it is. If it looked like the links and not normal text, that would be more clear.
fooker 24 hours ago [-]
Please do not try to understand Lean or proof assistants without first getting a rudimentary understanding of the logic involved. This article sort of skips over it, which is reasonable because it is pretty involved.
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
This is absolutely not a helpful list for someone who wants to prove things in lean, and just seems like weird gate-keeping. In particular, Proof Trees are completely irrelevant, incompleteness and compactness are only relevant if you are proving things in those specific fields and the only thing you need to know about constructive vs intuitionistic vs classical logic in lean is if you want to use the law of the excluded middle or some non-constructive proofs and tactics, lean won’t force that on you, so you sometimes need to “open classical”. (And this is covered in “Mathematics in Lean” and “Theorem Proving in Lean” at the appropriate place).
Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).
Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends https://leanprover-community.github.io/learn.html
I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.
But these aren’t things you necessarily need to do before getting started in lean.
6gvONxR4sf7o 21 hours ago [-]
Honestly, I'd say just play some of the lean games instead (https://adam.math.hhu.de/). I went through the dependent type theory and proof stuff first, and in hindsight it would have been much faster to just get the intuition first from learning to use a language like lean.
fooker 18 hours ago [-]
Sure, use whatever method of learning that works well for you.
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
seanhunter 14 hours ago [-]
I have absolutely no idea why you’re trying to make out that compactness for example is part of the theoretical foundations of Lean, but it definitely isn’t, and it’s so far off-base that I’m wondering why you’re saying things like this.
Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.
The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.
[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.
fooker 6 hours ago [-]
That's a different compactness :)
Math is full of fun overloads like this.
Most of my lean work involves software verification and transition systems. I suspect most people here would be interested in software verification rather than trying to solve unsolved math problems. You'd have a frustrating experience without the required logic background, from my experience dealing with a collaborator's new PhD students.
jvvw 13 hours ago [-]
I believe that compactness has a different meaning in topology than in logic btw (though my degree was so long ago now that I'm rusty on it all!).
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
seanhunter 8 hours ago [-]
That makes sense. You need no background in logic whatsoever to learn lean. For some reason that person was gate-keeping.
fooker 6 hours ago [-]
You need no background in anything to learn anything.
If you want to master it and use it effectively for something real, yeah some reading would help.
watt 14 hours ago [-]
Or, you could invest time in making a tool that can be used effectively without having to understand all the theoretical foundations. What's stopping you?
fooker 6 hours ago [-]
I don't know how to do it.
If someone would figure this out, the theoretical advancements they would discover on the way would likely earn them a Turing award.
auggierose 17 hours ago [-]
All of these things are definitely not necessary to know about to successfully use Lean, and not even useful to know for proving things in Lean.
IMO the experience of learning to use and understand a proof assistant gives one a pretty good foundation for then going deeper into logic and proof theory. I'm specifically thinking of Logical Foundations [0], which doubles as an introduction to Rocq and also an introduction to intuitionistic logic (and also type theory!).
Some specific disagreements:
- "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.
- Why is Gödel incompleteness necessary for one to understand how Lean works?
- Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.
You're crazy. Don't bother to try to understand lean's internal models unless you want to work on lean itself. Whatever style of proof you're used to, you can write in that style with mathlib.
fooker 18 hours ago [-]
> Whatever style of proof you're used to, you can write in that style with mathlib.
Yes, you can do that, and it'll be a frustrating experience.
Knowing the theoretical foundations of your tool is a great way to be happy and productive.
Without it you have issues similar to people trying to implement parsers with regex. :)
rramadass 18 hours ago [-]
What you actually need is knowledge of an overview of the Mathematics of Formal Methods in all their aspects viz. Predicate Logic, Set Theory, Temporal Logic, Type Systems etc.
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
whattheheckheck 18 hours ago [-]
Oh yeah let me just take another 4 years of undergrad to get a math degree too.
I thought this AI or SI was supposed to make shit easier for everyone.
fooker 18 hours ago [-]
Yeah artificial intelligence is an ideal solution to natural stupidity ;)
rramadass 18 hours ago [-]
That is just glib nonsense.
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
woggy 23 hours ago [-]
I’m curious whether people can use Lean primarily as a software specification language, without necessarily intending to prove everything.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
keeganryan 22 hours ago [-]
Yes, absolutely. There's been a lot of work along these lines in other interactive theorem provers like Isabelle/HOL and Rocq. The general term to search is "Hoare logic," and I'm also a fan of the Concrete Semantics textbook. Lean is a very flexible language, but the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed than Mathlib is for math.
the interface between specification and proof is not so clear, as one often has to look at the proof to understand the spec. And if we see something weird in the proof, that’s a good indication that something is off.
Yeah this is like if I say something is green how do you know that my green is your green? The proof of the mathematically modeled system is in no shape attached to the symbols that implement it unless its the same program or youre doing trace refinement. And then theres no way of proving that the program is correct in serving the business function unless you run it out. Quite computationally irreducible, the state machine of building state machines
lolakutty 19 hours ago [-]
[flagged]
whattheheckheck 18 hours ago [-]
Yeah if were going for knuths literate programming this is not it. We dont need 1000 lines of more code to prove another 100 lines. It needs to be more digestible and if its not possible then let's break out the licensing board to prove the ones who do understand this from those who dont
lolakutty 17 hours ago [-]
licensing board?
except for that I understood everything else you said..
watt 1 days ago [-]
This Lean stuff is gibberish and I don't understand why somebody thinks it's going to somehow make things better or simpler to understand.
fooker 1 days ago [-]
Perhaps when you don't understand something, your first step should be trying to understand it?
Especially when it is something other smart people have been advocating.
vouaobrasil 22 hours ago [-]
The thing is, it's not about making anything easier to understand. It's about padding academic CVs with something new.
poly2it 20 hours ago [-]
Gosh, all this academic nonsense like nuclear power and airplanes!
lolakutty 19 hours ago [-]
Hey, I think one could have built airplanes even if they never went to school.
watt 14 hours ago [-]
oh yes, academic proponents of aeronautics like Lord Kelvin and Simon Newcomb ?
Rendered at 22:39:14 GMT+0000 (Coordinated Universal Time) with Vercel.
A statement corresponds to a type and to proof that statement means to show that this type is inhabitetd (i.e., there is actually a value of that type).
A proof is then "just a program" in "just a programming language". Crucially, you do not care what "this program computes" but you care only that the program actually has the given type.
There is no concept of a "bug" in a proof term because you do not actually care what a proof term "computes". You care that it exists and that it is well typed.
https://proceedings.mlr.press/v306/ammanamanchi26a.html
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.
If you construct value of type `forall n, exists m, m≥n and m prime`, then you know you have such an object. Think of a `theorem` (the Lean keyword) as a function that returns such objects. If you try to return the wrong type (e.g. you build a `forall n, exists m, m≤n and m prime`) in your "function" body, you get a compile error. If you use types incorrectly in the middle (passing values and intermediate proofs to theorems incorrectly), you get a compile error.
It's just like any programming language except the type system is rich enough that in addition to being able to have a value x: Int, (so maybe x is 5) you can have values like h: x^2≥0 (so imagine h is some object you build that proves x^2≥0).
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
https://proceedings.mlr.press/v306/ammanamanchi26a.html
A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.
You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.
After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.
I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.
Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).
Excerpt:
The Rosetta Stone
Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.
A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."
This is generally untrue. The reason you don't have to remember is that your proof will inevitably rely on a theorem with "x ≠ 0" as one of the premises. (And if that doesn't happen, then the fact that lean defines division strangely isn't relevant to your proof.)
If what you're doing is writing code unaccompanied by proofs, then yes, this is something you'd have to remember.
If you're writing that theorem: Assuming you remember to include it in your premises.
Sometimes the invariant might not be mathematical, it might be social. I recall a story where 1/0 caused a problem because stock issuance uses a 0-share disbursement as a tombstone: to indicate that "this stock account has zeroed out this security and has no remaining ownership". You might not have remembered that and you might have forgotten to record that as a necessary invariant in your proofs. If lean had defined division to have a nonzero denominator, it would have caught the problem even if you didn't know that a zero share disbursement hada a different meaning.
1/0 is 0 in lean, though it may not be a problem. https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
* Constructive/Intuitionistic logic - https://en.wikipedia.org/wiki/Intuitionistic_logic
* Proofs and Types - https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
* (In)completeness - https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
* Compactness - https://en.wikipedia.org/wiki/Compactness_theorem
Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).
Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends https://leanprover-community.github.io/learn.html
One thing I would add is if you want to learn about proof writing in general there are a lot of good resources out there including “The Book of Proof” which is free online. https://rcsnyder.github.io/open-frontier-curriculum/07-resou...
I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.
But these aren’t things you necessarily need to do before getting started in lean.
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.
The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.
[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.
Math is full of fun overloads like this.
Most of my lean work involves software verification and transition systems. I suspect most people here would be interested in software verification rather than trying to solve unsolved math problems. You'd have a frustrating experience without the required logic background, from my experience dealing with a collaborator's new PhD students.
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
If you want to master it and use it effectively for something real, yeah some reading would help.
If someone would figure this out, the theoretical advancements they would discover on the way would likely earn them a Turing award.
https://rcsnyder.github.io/open-frontier-curriculum/07-resou...
Some specific disagreements:
- "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.
- Why is Gödel incompleteness necessary for one to understand how Lean works?
- Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.
[0] https://softwarefoundations.cis.upenn.edu/lf-current/index.h..., and see also its sequel Programming Language Foundations [1].
[1] https://softwarefoundations.cis.upenn.edu/plf-current/index....
[1] https://en.wikipedia.org/wiki/Natural_deduction
Yes, you can do that, and it'll be a frustrating experience.
Knowing the theoretical foundations of your tool is a great way to be happy and productive.
Without it you have issues similar to people trying to implement parsers with regex. :)
Towards that end I highly recommend the following books;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke - An easy-to-read book needed for background mathematical fundamentals.
2) Understanding Formal Methods by Jean-Francois Monin - This gives an excellent overview of the core topics and a must-read. From here you can branch off into studying any specific approach and its tool (eg. Lean4/TLA+/etc.). Once you have studied this there is nothing "Formal" (specification/verification/etc.) which is impenetrable.
3) The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - Walks you through the entire process of deriving a program using successive refinements from specifications using Hoare/Dijkstra approach.
I thought this AI or SI was supposed to make shit easier for everyone.
The above books do not need a math degree; You just need to become "familiar" with the mathematical form and its jargon. Most programmers can read and understand them.
You can easily finish the books in a couple of months using AI for clarifying/simplifying difficult concepts to gain quicker understanding.
AI can produce all the How but the What/Why still needs to happen in your head and hence the need to understand the mathematics.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
Yeah this is like if I say something is green how do you know that my green is your green? The proof of the mathematically modeled system is in no shape attached to the symbols that implement it unless its the same program or youre doing trace refinement. And then theres no way of proving that the program is correct in serving the business function unless you run it out. Quite computationally irreducible, the state machine of building state machines
except for that I understood everything else you said..
Especially when it is something other smart people have been advocating.