FINITE: Formalize the magma cohomology approach and use it to refute implications
Opened this issue · 0 comments
teorth commented
In particular, develop enough API for the cohomological constructions in https://teorth.github.io/equational_theories/blueprint/cohomology-chapter.html that the examples described in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/485516710 could be verified in Lean without extra heartbeats. In particular this could supersede #953.
When done, update Conjectures.lean and add \lean and \leanok to blueprint results as appropriate.