Lean – Theorem Prover

https://leanprover.github.io/

by thunderbong • 4 years ago

101 29 4 years ago

leanprover.github.io

agentultra2• 4 years ago

Also interesting as a programming language:

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

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

daxfohl• 4 years ago

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.

agentultra2• 4 years ago

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

dunham• 4 years ago

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.

nolroz• 4 years ago

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

zone411• 4 years ago

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.

deadbeef572• 4 years ago

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.

nequo2• 4 years ago

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/

kevinbuzzard2• 4 years ago

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.

deterministic4• 4 years ago

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.

deterministic4• 4 years ago

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.

dang• 4 years ago

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)

schoen• 4 years ago

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

vicpara• 4 years ago

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?

nequo2• 4 years ago

What specifically is crazy about Lean's syntax?

deadbeef572• 4 years ago

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.

sakras• 4 years ago

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?

jroesch• 4 years ago

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

nextos• 4 years ago

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

deterministic4• 4 years ago

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.

moloch-hai2• 4 years ago

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

wetmore• 4 years ago

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

marcus_• 4 years ago

Not necessarily. Lean allows for axiom of choice.

andrepd• 4 years ago

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.

alimw• 4 years ago

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

deterministic4• 4 years ago

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

voytec• 4 years ago

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

Lean – Theorem Prover

Related Stories