Number of equations on the hypothesis

Stream: Equational

[Andrés Goens]

I notice the project asks for implications of the form $\text{EquationN} \Rightarrow \text{EquationM}$, i.e. wether a single equation implies another one, instead of having (a conjuction/implication of) multiple equations on the LHS/as the hypothesis. I'm curious, is there a reason for this other than this is already complex enough as a start?

[Vlad Tsyrklevich]

There's some discussion of this in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Resolving.20.20.3E60.25.20of.20cases.20with.20non-implications.20automatically and #Equational > Efficent representation of refutations At least for non-implications, this is much much more efficient computationally.

[Andrés Goens]

Vlad Tsyrklevich said:

There's some discussion of this in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Resolving.20.20.3E60.25.20of.20cases.20with.20non-implications.20automatically and #Equational > Efficent representation of refutations At least for non-implications, this is much much more efficient computationally.

Hmm, I can't find it in either :shrug: do you have a link to the concrete message?

[Vlad Tsyrklevich]

Sorry, I was referring to https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Resolving.20.20.3E60.25.20of.20cases.20with.20non-implications.20automatically/near/473040774 and https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Efficent.20representation.20of.20refutations/near/473055469

[Vlad Tsyrklevich]

I haven't been able to find a way locally to make it work for implication in a way that appears to save time? But I'm sure I could be missing something

[Terence Tao]

This is an artificial restriction on my part to try to make the initial pilot project feasible to complete, while still highly nontrivial computationally. The stated aim is in some sense a "MacGuffin" intended to figure out how to organize large scale collaborations between humans and automated tools via Lean; once this goal is completed, then presumably we can adapt it to many more interesting tasks (most obviously, studying more complicated relations between laws than equations, but also perhaps some problems outside of universal algebra as well).