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.
> 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.
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.
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.
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.
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.
> 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.
OP: Your article shows “[Contents]” where presumably the table of contents is to be displayed.
It's a button
So it is. If it looked like the links and not normal text, that would be more clear.
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.
* 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
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.
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.
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.
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.
The thing is, it's not about making anything easier to understand. It's about padding academic CVs with something new.
Gosh, all this academic nonsense like nuclear power and airplanes!