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.
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.
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.
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.
> 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).
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.
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.
> 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.
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.
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).
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.
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.
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.
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.
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?
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.
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.
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.
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.
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.
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
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
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.
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).
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).
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.
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
https://rcsnyder.github.io/open-frontier-curriculum/07-resou...
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.
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. :)
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.