from Hacker News

Theorem Proving in Lean

by benwr on 5/28/18, 7:39 AM with 30 comments

  • by agentultra on 5/28/18, 6:37 PM

    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.

  • by aban on 5/28/18, 3:42 PM

    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

  • by 4rgento on 5/28/18, 6:55 PM

    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/

  • by logicchains on 5/29/18, 4:53 AM

    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.

  • by YorkshireSeason on 5/29/18, 1:22 PM

    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/

  • by robinhoode on 5/29/18, 12:54 AM

    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.

  • by sevensor on 5/29/18, 1:35 PM

    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.

  • by tmpmov on 5/29/18, 3:12 AM

    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?

  • by amelius on 5/29/18, 10:17 AM

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

  • by qwerty456127 on 5/28/18, 9:09 PM

    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?