search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
https://teorth.github.io/equational_theories/
Apache License 2.0
204 stars 49 forks source link

SUBGRAPH: Add the implications/anti-implications between 168 and the other equations as conjecture statements. #35

Closed teorth closed 1 month ago

few commented 1 month ago

I'm not sure what exactly should happen here. In #103, I have a number of theorems involving equation 168 and others for which a similar issue exists.

teorth commented 1 month ago

If you already have some implications relating 168 with other Subgraph equations, you can import the relevant Lean file into Subgraph.lean and maybe make a comment within the Subgraph.lean file of the relevant implications that come from imports. (Eventually, our automated tools should be able to work out what all the available implications are from scraping the relevant Lean files, but in any event a human-readable comment is also useful.) Any remaining implications involving 168 that you are unsure of can be left as conjectures (if you have a good guess whether the implication is true or false), or as a comment that the implication is open. You can report all this on this issue and I can then assign further tasks accordingly to resolve the remaining conjectures.

teorth commented 1 month ago

Closing due to obsolete workflow now that more automated tools are available.