Theorem Proving in Lean

As far as theorem provers go Coq seems to be the most widely known among working programmers.<p>Lean deserves wide recognition. First, it&#x27;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.<p>If you have only heard about interactive theorem provers and don&#x27;t yet have any opinions I&#x27;d give Lean a try first. The interactive tutorials are nice and the aforementioned features make it pleasant to work with.

An Introduction to Lean [0] is another nice (albeit incomplete) tutorial.<p>There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help.<p>[0]: <a href="https:&#x2F;&#x2F;leanprover.github.io&#x2F;introduction_to_lean&#x2F;" rel="nofollow">https:&#x2F;&#x2F;leanprover.github.io&#x2F;introduction_to_lean&#x2F;</a><p>[1]: <a href="https:&#x2F;&#x2F;leanprover.zulipchat.com" rel="nofollow">https:&#x2F;&#x2F;leanprover.zulipchat.com</a>

Obligatory mention to `coq` and `Software foundations`(SF).<p>`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&#x27;m able to see the patterns in most mathematicals proof I come by.<p>Must read book if you want to acquire mathematical superpowers.<p>Coq tells you when you are wrong, but it doesn&#x27;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&#x27;ll even be able to spot slopy proof in text books.<p>[0]<a href="https:&#x2F;&#x2F;softwarefoundations.cis.upenn.edu&#x2F;" rel="nofollow">https:&#x2F;&#x2F;softwarefoundations.cis.upenn.edu&#x2F;</a>

Interesting note: a new version, Lean 4, is currently under development, which will presumably replace Lean 3 once complete: <a href="https:&#x2F;&#x2F;github.com&#x2F;leanprover&#x2F;lean&#x2F;blob&#x2F;master&#x2F;doc&#x2F;lean4.md" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;leanprover&#x2F;lean&#x2F;blob&#x2F;master&#x2F;doc&#x2F;lean4.md</a>.

One should also mention <i>Isabelle&#x2F;HOL</i> [1] and <i>Concrete Semantics</i> [2]. As of May 2018, Isabelle&#x2F;HOL has the best proof automation, in case you want to get things done.<p>[1] <a href="https:&#x2F;&#x2F;isabelle.in.tum.de&#x2F;" rel="nofollow">https:&#x2F;&#x2F;isabelle.in.tum.de&#x2F;</a>

This seems really cool!<p>Unfortunately I can&#x27;t seem to get the live compiler to work properly. I get this message when I check the JS console:<p>Failed to execute &#x27;postMessage&#x27; on &#x27;DedicatedWorkerGlobalScope&#x27;: DOMException object could not be cloned.

I&#x27;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&#x27;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&#x27;t find a solid answer. Was there a fork version 2 that continues development with HoTT?

Hmm, in the example, I tried to change<p><pre><code> show p ∧ q </code></pre> into<p><pre><code> show p ∧ p </code></pre> (which should also be true). But it gives a type error.<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?