<story><title>Doing a math assignment with the Lean theorem prover</title><url>https://ahelwer.ca/post/2020-04-05-lean-assignment/</url></story><parent_chain></parent_chain><comment><author>xvilka</author><text>The same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq &amp;quot;war&amp;quot; and so-called &amp;quot;setoid hell&amp;quot; you can read a lengthy discussion on their GitHub[6].&lt;p&gt;[1] &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;coq.inria.fr&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;coq.inria.fr&amp;#x2F;&lt;/a&gt;&lt;p&gt;[2] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;learnxinyminutes.com&amp;#x2F;docs&amp;#x2F;coq&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;learnxinyminutes.com&amp;#x2F;docs&amp;#x2F;coq&amp;#x2F;&lt;/a&gt;&lt;p&gt;[3] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;coq&amp;#x2F;coq&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;coq&amp;#x2F;coq&lt;/a&gt;&lt;p&gt;[4] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;softwarefoundations.cis.upenn.edu&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;softwarefoundations.cis.upenn.edu&amp;#x2F;&lt;/a&gt;&lt;p&gt;[5] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;coq.discourse.group&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;coq.discourse.group&amp;#x2F;&lt;/a&gt;&lt;p&gt;[6] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;coq&amp;#x2F;coq&amp;#x2F;issues&amp;#x2F;10871&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;coq&amp;#x2F;coq&amp;#x2F;issues&amp;#x2F;10871&lt;/a&gt;</text></comment>
<story><title>Doing a math assignment with the Lean theorem prover</title><url>https://ahelwer.ca/post/2020-04-05-lean-assignment/</url></story><parent_chain></parent_chain><comment><author>logicchains</author><text>For people interested in using Lean, note that there&amp;#x27;s a community fork (&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover-community&amp;#x2F;lean&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover-community&amp;#x2F;lean&lt;/a&gt;) of the last official Lean 3 release 3.4.2 (&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean&lt;/a&gt;). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean4&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;leanprover&amp;#x2F;lean4&lt;/a&gt;), and it&amp;#x27;s not clear when that will be ready).</text></comment>