Interesting project for anyone who want to start learning lean and contribute to a project.
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.
The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.
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.
There'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.
Comments
Interesting project for anyone who want to start learning lean and contribute to a project.
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.
The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.
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.
There'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.
partial visualization of the (WIP) graph: https://github.com/teorth/equational_theories/blob/0e67dad3b...
outline of the project: https://teorth.github.io/equational_theories/blueprint/
github repo: https://github.com/teorth/equational_theories
Sounds exactly like Truth Mining in Greg Egan's Diaspora.