The Type Theory Forall podcast published an interview this week with Kevin Buzzard who has been coordinating the mathlib efforts[1] for Lean. If you're interested in math, theorem provers, or Lean, then it is worth listening to:
Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I think it has the potential to change mathematics. But it is coordinated by many people, like many open source projects.
Thanks for doing the interview Kevin. I have learned a lot from your articles and interviews over the years. Especially how different the math I care about (computation) is from the math that mathematicians care about (structure).
It is great to see that with Lean/mathlib computer scientists and mathematicians have found a way to work together and benefit from the insights and skills of each other.
So please continue doing what you are doing. I believe it will long term have a massive positive impact on both computer science and mathematics.
Thanks! I just listened to it. What a great interview.
It made me realise yet again that the math used by computer scientists is usually different from the math used by mathematicians. Because what computer scientists care about (computations and proofs) is very different from what mathematicians care about (structures and proofs).
Which means that computer scientists often choose a different foundation for the mathematics they use. Set theory is but one possible foundation. However other foundations (based on type theory for example) are more useful for computer scientists. Resulting in a different flavour of mathematics. And things that are proven to be true in one foundation isn’t necessarily true in another foundation.
However it is all still math. Just different flavours of math based on different foundational axioms.
Is the experience here much different from Idris? The latter was more a language that can also be used for proofs, whereas Lean came out of a proof assistant. Does that lead to much difference in use, or do the approaches essentially converge?
Looking briefly at the example code, it seems pretty similar.
I did advent of code in Lean4 in 2022 and Idris2 in 2021. Lean4 was fairly similar to Idris code-wise.
Minor differences:
- On the Lean side I leveraged the fact that Arrays can mutate in place (if the refcount is 1). For Idris I'd use a Buffer (IO Monad) or SortedMap.
- Lean has a nice mechanism where I can drop an #eval or #check in the code and have the result show up in an editor pane. For most days, I never compiled/ran the code separately.
- Lean defaults to total, so I had to put partial in a couple of places.[1]
- Lean could have accepted proofs that my indices were in range, but I used the unsafe functions instead.[2]
- Idris has some nice editor functionality to stub out functions and case splits for you.
[1]: Idris2 defaults to "covering", which says case splits have to cover, but relaxes termination checking. A couple of the spots where I put partial in lean could be proven total, but I was not familiar with the theorem proving corner of lean. Idris totality checking is slightly different in that you can't add proofs, but I think you can achieve the same results by adding additional arguments.
[2]: Because I didn't know the theorem proving bits, but I intend to go back and try to patch these up as an exercise.
I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics.
Note that the sudden drop-off at the end of the graph that shows commits-per-month is because this is measuring commits-to-mathlib3. A lot of contributors are currently helping with the port-to-mathlib4 (aka the Lean 4 version of mathlib). Unfortunately there is not yet a fancy graph showing the growth of mathlib4.
As someone who’s never messed with a theorem prover but would like to, would it make sense to start with Lean? How is it different from Coq? And is Coq worth learning before Lean?
Did a PhD half focused on verification and also very biased being an early Lean developer. imo the Lean tooling and everything is much better I personally would never use Coq again especially after writing 200kloc+ of it over a few years.
It has improved a lot but still I think Lean has many things going for it including a large focus on programming and using your Lean programs directly (versus extraction, which is roughly a really shitty compiler from Coq to Ocaml or another extracted language).
Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.
I would recommend starting with Idris. It has all the power of a typical theorem prover but feels like a cool programming language. It also has a great book to bring you up to speed: “Type Driven Development”.
The perhaps surprising thing about theorem provers is that you do not use them to prove theorems. That is, you only use them on theorems you have already proven, and the use is to persuade other people that your proof is valid.
Otherwise I guess you would call it a "conjecture prover".
Interactive theorem provers, perhaps, though I guess they also allow for exploratory use (though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true).
But automated theorem provers (e.g. for first-order logic, SAT, or SMT), they can and have been used to solve open problems in mathematics: the famous four-color theorem, but many others.
> though I'm not sure anyone ever used an interactive theorem prover to show a conjecture they did not know was true
The Liquid Tensor Experiment [1] formalised a proof that the author himself found sufficiently complicated to have doubts about. And at a very different level, I myself began to formalise a proof [2] while it still had at least one hole in it. I was fortunate it turned out to be true!
If not, you could have published a proof that it was not.
I knew somebody whose PhD project was a proof that all objects X are in Y. After rather some time he found instead that there are no objects X. That proof was not considered PhD material, although it seems like it should have been.
Why on earth they had to invent a new language with another crazy syntax that reinvents everything?
With such an incredible team at MSR that did everything from new languages and compilers, couldn't they have know better?
There are several new and non-trivial things going on in this language! Look at the papers about hygienic macros, or functional-but-in-place, or any of the others.
https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard...
[1] https://leanprover-community.github.io/