MODIFIED_GREEDY: Refute 1692 -> 47, 1832, 2441, 3050, 3456, 4065

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

265 stars 58 forks source link

MODIFIED_GREEDY: Refute 1692 -> 47, 1832, 2441, 3050, 3456, 4065 #607

Open teorth opened 1 month ago

teorth commented 1 month ago

See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Proposed.20new.20target.3A.2063.20and.201692.20.28.22Dupont.20and.20Dupond.22.29/near/477252513 for the human-readable proof.

The formal proof can go in the ManuallyProved folder. ManuallyProved.lean should be updated afterwards, and the appropriate conjectures from Conjectures.lean removed.

Aaron1011 commented 1 month ago

claim