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.

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.

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

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.

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.

This tutorial starts by explaining how things work, and only later shows you magic. That's exactly what I like about it, actually. Almost every coq tutorial I found (I tried software foundations, cpdt, and several shorter online tutorials) fails to explain what you're doing before you do it.

Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.

What's the upside compared to coq?

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

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/

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.

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/

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.

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

Whoops, forgot to link to _Concrete Semantics_.

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

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.

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

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.

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?

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.

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

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)

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.

There are tons of other ways of writing the same thing in Lean too, of course. Here is one:

    theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
    begin intros, simp * end

https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...

In Lean you could do

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc

for a tactic proof and

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩

for a term proof (just write down the function).

Cool, thanks for this. I've yet to play with Lean, but it looks very interesting! (I'm hoping that my time invested in Coq will transfer reasonably well...)

You're welcome! I'm in a similar boat, coming to this tutorial from a Coq background (and some Isabelle/HOL). I'm pleasantly surprised how similar many things are. But I'm also a bit disappointed because I was under the impression that Lean was relying on automation via Z3 a lot more. Not quite done with the tutorial yet, so there might still be some material to this effect coming up, but I'm afraid not.

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?

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.

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