TREE: Refute 1447 -> 1429, 4269
Closed this issue · 2 comments
teorth commented
There is an explicit construction given in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/713.2C.201289.2C.201447/near/482236139 which would work without any greedy construction. Alternatively, one can try to formalize the ATP-powered greedy construction, discussed at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/713.2C.201289.2C.201447/near/481629774
This would go in the ManuallyProved folder. When done, update ManuallyProved.lean and Conjectures.lean.
goens commented
claim