<story><title>A pilot project in universal algebra to explore new ways to collaborate</title><url>https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/</url></story><parent_chain></parent_chain><comment><author>gryn</author><text>Interesting project for anyone who want to start learning lean and contribute to a project.&lt;p&gt;The project as described in the article is to produce a graph (Poset) where each node is a law (say the commutativity equation for example) and each edge is either a proof of implication or a proof of a non-implication, since this graph is infinite the project limits the laws considered to up to 4 applications of the binary operator.&lt;p&gt;The main goal is not the proofs themselves but experimenting in doing math in a matter that&amp;#x27;s more similar to software engineering in the open source community.&lt;p&gt;The collaborative aspect of the project is to write a proof for each kind of edge (implication and not_implications) between the 4694 considered nodes.&lt;p&gt;There&amp;#x27;s also the advantage that a GitHub CI running lean will be setup to automatically check if the pull requests adding theses edges are right or wrong without the need for a human to do the checking of the proofs in their head.&lt;p&gt;partial visualization of the (WIP) graph: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;teorth&amp;#x2F;equational_theories&amp;#x2F;blob&amp;#x2F;0e67dad3bd075782060452d3c604544198975080&amp;#x2F;images&amp;#x2F;implications.svg&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;teorth&amp;#x2F;equational_theories&amp;#x2F;blob&amp;#x2F;0e67dad3b...&lt;/a&gt;&lt;p&gt;outline of the project: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;teorth.github.io&amp;#x2F;equational_theories&amp;#x2F;blueprint&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;teorth.github.io&amp;#x2F;equational_theories&amp;#x2F;blueprint&amp;#x2F;&lt;/a&gt;&lt;p&gt;github repo: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;teorth&amp;#x2F;equational_theories&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;teorth&amp;#x2F;equational_theories&lt;/a&gt;</text></comment>
<story><title>A pilot project in universal algebra to explore new ways to collaborate</title><url>https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/</url></story><parent_chain></parent_chain><comment><author>davidrjones1977</author><text>I really love the extent to which Terry Tao has embraced the promise and potential of proof assistants. So many smart and talented people in that community doing so much amazing work. With folks like these pushing the boundaries, the sky is the limit.</text></comment>