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.
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.
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.
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.
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?
Hmm, in the example, I tried to change
show p ∧ q
show p ∧ p
I guess I better start reading the tutorials ...
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?
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.