Theorem Proving in Lean

Theorem Proving in Lean(leanprover.github.io)

156 points by benwr 8 years ago | 30 comments

agentultra 8 years ago |

As far as theorem provers go Coq seems to be the most widely known among working programmers.

Lean deserves wide recognition. First, it's fast enough for highly interactive theorem development. Second it can also be used as a programming language. And lastly its syntax is pleasant to work with which is important to the experience.

If you have only heard about interactive theorem provers and don't yet have any opinions I'd give Lean a try first. The interactive tutorials are nice and the aforementioned features make it pleasant to work with.

tathougies 8 years ago | |

These are interesting pros for lean. I just wanted to point out that Coq is also a programming language, and there are some packages of hackage of various data structures proven correct in Coq and then compiled from the original coq sources.

agentultra 8 years ago | | |

I have read a fair bit about use of hs-to-coq and coq-haskell; Coq is a nice tool for sure!

benwr 8 years ago | |

Strongly agree. I only found Lean after a couple of weeks of struggling to pick up coq. In my opinion, this tutorial alone makes lean a better choice for beginners.

tom_mellior 8 years ago | | |

Out of interest, what about this tutorial do you find better than (which?) Coq tutorials?

I think Lean might be the better technology, but I don't think this tutorial is better than Software Foundations. I can't see beginners not being turned off by boring discussions of hierarchies of universes before the first real proofs to get you hooked.

elcapitan 8 years ago | |

What's the upside compared to coq?

aban 8 years ago |

An Introduction to Lean [0] is another nice (albeit incomplete) tutorial.

There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help.

[0]: https://leanprover.github.io/introduction_to_lean/

[1]: https://leanprover.zulipchat.com

4rgento 8 years ago |

Obligatory mention to `coq` and `Software foundations`(SF).

`coq` is an amazing piece of software. SF makes you start prooving thing right from chapter one. Learn mathematics by doing. After going through the chapters of Logic Foundations I'm able to see the patterns in most mathematicals proof I come by.

Must read book if you want to acquire mathematical superpowers.

Coq tells you when you are wrong, but it doesn't provide you the solution either. So you have to work it up for yourself. The satisfaction of finding a proof and knowing it is right is hard to match( this is known as the video-game-effect). You'll even be able to spot slopy proof in text books.

[0]https://softwarefoundations.cis.upenn.edu/

logicchains 8 years ago |

Interesting note: a new version, Lean 4, is currently under development, which will presumably replace Lean 3 once complete: https://github.com/leanprover/lean/blob/master/doc/lean4.md.

YorkshireSeason 8 years ago |

One should also mention Isabelle/HOL [1] and Concrete Semantics [2]. As of May 2018, Isabelle/HOL has the best proof automation, in case you want to get things done.

[1] https://isabelle.in.tum.de/

unboxed_type 8 years ago | |

True. It is worth pointing out that Isabelle/HOL does not have dependent types in its underlying logic making framework building a (much?) harder work.

YorkshireSeason 8 years ago | | |

I'm not sure what you mean by "framework building" in this context.

YorkshireSeason 8 years ago | |

Whoops, forgot to link to _Concrete Semantics_.

[2] http://www.concrete-semantics.org

robinhoode 8 years ago |

This seems really cool!

Unfortunately I can't seem to get the live compiler to work properly. I get this message when I check the JS console:

Failed to execute 'postMessage' on 'DedicatedWorkerGlobalScope': DOMException object could not be cloned.

benwr 8 years ago | |

This problem went away for me when I turned off my ad blocker.

sevensor 8 years ago |

I've got very little experience with theorem provers, but I have spent some time working through this book, and I can recommend it. If you're interested, the Emacs Lean mode works great.

tmpmov 8 years ago |

Was there a reason for the move away from HoTT? I seem to recall looking this up a while ago but didn't find a solid answer. Was there a fork version 2 that continues development with HoTT?

im_down_w_otp 8 years ago | |

This was a discussion I remember coming across not long ago when I had the same question: https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIz...

There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3

Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think Lean 2 started life intending to handle HoTT either.

amelius 8 years ago |

Hmm, in the example, I tried to change

    show p ∧ q

into

    show p ∧ p

(which should also be true). But it gives a type error.

I guess I better start reading the tutorials ...

tom_mellior 8 years ago | |

That is also true, but its proof is different. Proofs have types; the "and.intro hq hp" part has type "q /\ p". If you change it to "and.intro hp hp", you can prove "p /\ p". That is, the following works:

    theorem and_commutative (p q : Prop) : p ∧ q → p ∧ p :=
    assume hpq : p ∧ q,
    have hp : p, from and.left hpq,
    have hq : q, from and.right hpq,
    show p ∧ p, from and.intro hp hp

(and then you should rename it from "and_commutative" to something else, and you can remove the "hq" line)

gmfawcett 8 years ago | | |

Just for the sake of comparison, the same proof in Coq might be written:

    Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof.
      intros [HP HQ].
      split.
        - apply HQ.
        - apply HP. 
    Qed.

"intros [HP HQ]" separates the two conjuncts of the hypothesis into separate hypotheses (P, and Q); "split" breaks the goal (Q ∧ P) into two subgoals (Q, and P), and the two applications prove the two subgoals.

It could also be written:

    Theorem and_commutative_2 (P Q : Prop) : P ∧ Q → Q ∧ P.
    Proof. tauto. Qed.

...as the proof tactic "tauto" is capable of proving this (simple) theorem immediately.

qwerty456127 8 years ago |

Is there something like this that can use a real data set to validate all the statements against instead of a set of hand-written formal assumptions?

nickpsecurity 8 years ago | |

Look up the words Dynamic Invariant Generation. Uses examples or test data. There's also machine learning techniques for pulling the specs out of combos of input and output. Human still has to check them for correctness. I have seen folks use automated proof or test generation to reality check them, though.

alimw 8 years ago | |

Do you maybe want a database integrated with a good logic programming language? Datomic/Datalog springs to mind.

theorem and_commutative (p q : Prop) : p ∧ q → p ∧ p := assume hpq : p ∧ q, have hp : p, from and.left hpq, have hq : q, from and.right hpq, show p ∧ p, from and.intro hp hp