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
257 stars 57 forks source link

LARGE GREEDY: Refute all implications from 713, 1289 #771

Open teorth opened 3 weeks ago

teorth commented 3 weeks ago

As discussed in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1076.20!.3D.3E.203/near/476933251 , we have in principle a formalized proof of these implications, but they are extremely large.

Specifically, we need

conjecture Equation713facts : ∃ (G : Type) ( : Magma G), Facts G [713] [817, 1426, 3862, 4065]

conjecture Equation1289facts : ∃ (G : Type) ( : Magma G), Facts G [1289] [3116, 4435]

See further discussion at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Remaining.20unformalized.20theorems.3F/near/479985776 and https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/713.2C.201289.2C.201447

1447 has been removed from this list as it has been proven by other means.

Proof can go in the ManuallyProved folder. When done, update ManuallyProved.lean, Conjectures.lean and add \lean and \leanok's to the blueprint.

teorth commented 5 days ago

Alternate proofs of 713, 1289 available at https://teorth.github.io/equational_theories/blueprint/infinite-magma-constructions-chapter.html#greedy-section