Lean – Theorem Prover | Hacker News Reader

Lean – Theorem Prover

leanprover.github.io

101 pointsthunderbong29 comments

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:

https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard...

[1] https://leanprover-community.github.io/

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.

If you want to try it out and have never used a theorem prover, consider trying the Natural Number Game.

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...

Also interesting as a programming language:

Lean 3: https://agentultra.github.io/lean-for-hackers/

Lean 4: https://agentultra.github.io/lean-4-hackers/

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 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.

[0] https://github.com/leanprover-community/mathlib

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.

Here is a chart of Mathlib's growth: https://leanprover-community.github.io/mathlib_stats.html, and here is information about what parts of undegrad math are covered so far: https://leanprover-community.github.io/undergrad.html.

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).

However, the amount of teaching material focusing on software verification using Lean is frustratingly small?

Coq has FRAP and CPDT [1], which teach you most techniques that are used in industry. Also Software Foundations.

AFAIK, there's a version of Concrete Semantics using Lean [2]. But that's still just semantics.

Any other materials focused on software verification, not on formalizing mathematics?

[1] http://adam.chlipala.net

[2] https://news.ycombinator.com/item?id=22794533

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”.

It will blow your mind.

The future of interactive theorem proving? - https://news.ycombinator.com/item?id=32489099 - Aug 2022 (16 comments)

The Lean Theorem Prover - https://news.ycombinator.com/item?id=30752610 - March 2022 (1 comment)

Propositional logic exercises with the lean theorem prover - https://news.ycombinator.com/item?id=28951457 - Oct 2021 (8 comments)

The Natural Number Game - https://news.ycombinator.com/item?id=27504877 - June 2021 (2 comments)

A Review of the Lean Theorem Prover - https://news.ycombinator.com/item?id=25550240 - Dec 2020 (11 comments)

Lean is better for proper maths than all the other theorem provers - https://news.ycombinator.com/item?id=22802490 - April 2020 (1 comment)

Natural number game - https://news.ycombinator.com/item?id=22801607 - April 2020 (14 comments)

Lean Book: The Hitchhiker's Guide to Logical Verification [pdf] - https://news.ycombinator.com/item?id=22794533 - April 2020 (19 comments)

Doing a math assignment with the Lean theorem prover - https://news.ycombinator.com/item?id=22789953 - April 2020 (29 comments)

Coq is a Lean Typechecker - https://news.ycombinator.com/item?id=22171305 - Jan 2020 (31 comments)

Theorem Proving in Lean [pdf] - https://news.ycombinator.com/item?id=21108357 - Sept 2019 (22 comments)

Theorem Proving in Lean - https://news.ycombinator.com/item?id=17171101 - May 2018 (30 comments)

Theorem Proving in Lean - https://news.ycombinator.com/item?id=9424507 - April 2015 (1 comment)

Tutorial: Theorem Proving in Lean - https://news.ycombinator.com/item?id=9288135 - March 2015 (2 comments)

Also related and interesting:

https://news.ycombinator.com/threads?id=kevinbuzzard

Mathematicians welcome computer-assisted proof in ‘grand unification’ theory - https://news.ycombinator.com/item?id=27559917 - June 2021 (136 comments)

Formalising Mathematics: An Introduction - https://news.ycombinator.com/item?id=26214593 - Feb 2021 (116 comments)

A mathematical formalisation challenge by Peter Scholze - https://news.ycombinator.com/item?id=25322551 - Dec 2020 (24 comments)

At the International Mathematical Olympiad, computers prepare to go for the gold - https://news.ycombinator.com/item?id=24544607 - Sept 2020 (64 comments)

Division by zero in type theory: a FAQ - https://news.ycombinator.com/item?id=23745532 - July 2020 (82 comments)

Where is the fashionable mathematics? - https://news.ycombinator.com/item?id=22390486 - Feb 2020 (64 comments)

Proper link: https://leanprover.github.io/about/

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".

The proof is constructive though, so that's something.

Not necessarily. Lean allows for axiom of choice.

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!

[1] https://leanprover-community.github.io/blog/posts/lte-final/ [2] https://github.com/agjftucker/exists-unique

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.

Theorem provers are used all the time to prove new things in computer science. A few examples: CompCert, SeL4 etc.

Sheesh. I got all excited thinking that Lean was working on "Thorium Power".

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?

What specifically is crazy about Lean's syntax?

Please take a look at the papers about Lean (https://leanprover-community.github.io/papers.html) and explain to me how that "reinvents everything".

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.

Reply on news.ycombinator.com