Equation 5105 -> Equation 2

Stream: Equational

[Daniel Weber]

The question of whether Equation 5105 implies that a magma is nontrivial is open. However, as Equation5105 is in Equations.lean, we'll have to resolve that to complete the implication graph.

How should we go about this?

[David Renshaw]

Maybe we ignore all equations whose ID is greater than 4694?

[David Renshaw]

Currently there are 3 such: https://github.com/teorth/equational_theories/blob/2572c835abdd665eb7f1a771e9855dceb7c05d1f/equational_theories/Equations.lean#L120-L129

[Daniel Weber]

David Renshaw said:

Maybe we ignore all equations whose ID is greater than 4694?

That would be fun, as that reduces the number of unknown implications to 1121 :smile:

[David Renshaw]

how? Shouldn't it at most reduce by (3 * 4097)?

[Daniel Weber]

6 * 4097, the implications have two directions

[David Renshaw]

well, then we're a lot closer to being done that I had thought!

[Terence Tao]

We can make a distinction between the "Core" implication graph (only up to 4694, and the original goal of the project) and the "Expanded" implication graph. The dashboard could ideally list both statistics, and the equation explorer could have an option to view either core or expanded data. And the automated tools could be made to run on expanded data. Hmm, that's a lot of tasks, not sure how to split it into issues neatly. EDIT: equational#378 and equational#379

[Amir Livne Bar-on]

Up to equivalence it's only 724 696 unknown implications

EDIT: include counter-examples with linear operators

[Amir Livne Bar-on]

And to completely resolve order 3, only 16 are needed:

Equation65 => Equation359
Equation73 => Equation99
Equation73 => Equation125
Equation73 => Equation203
Equation73 => Equation229
Equation73 => Equation255
Equation118 => Equation222
Equation118 => Equation274
Equation229 => Equation73
Equation229 => Equation125
Equation274 => Equation47
Equation274 => Equation99
Equation274 => Equation118
Equation274 => Equation203
Equation274 => Equation222
Equation261 => Equation307

[David Renshaw]

equational#381 updates the dashboard

[Terence Tao]

Amazing that we can get more than an order of magnitude reduction in the outstanding implications just by fixing an accounting error

[David Renshaw]

it's like writing an essay for school and waiting until the last minute to switch from single-spaced lines to double-spaced lines

[Nicholas Carlini]

This might answer the confusion I had in equational#380 where my counting was off from --hist.

[Terence Tao]

@Amir Livne Bar-on Can you also make a list of the 696 unknown implications? I am planning on adding them to the "statistics and data files from a given point in time" portion of README.

[Amir Livne Bar-on]

unknowns_10_06.txt

These are the current unknown implications up to order 4, and up to equivalence. The file includes the 696 truly unknown + 36 that are disproved by Vampire but the proof isn't formalized in Lean. The 36 known-false-but-missing-proof ones are marked with (*).

[Terence Tao]

OK, now added to readme. I see the dashboard has updated to a very pleasing 99.995% completion rate. At this point having a time series for the project may in fact become moot.

696 implications to go! (Maybe even less, if we use duality.)

[Will Sawin]

Amir Livne Bar-on said:

And to completely resolve order 3, only 16 are needed:

Equation65 => Equation359
Equation73 => Equation99
Equation73 => Equation125
Equation73 => Equation203
Equation73 => Equation229
Equation73 => Equation255
Equation118 => Equation222
Equation118 => Equation274
Equation229 => Equation73
Equation229 => Equation125
Equation274 => Equation47
Equation274 => Equation99
Equation274 => Equation118
Equation274 => Equation203
Equation274 => Equation222
Equation261 => Equation307

All of these look like it might be possible to prove the implications hold in finite magmas. The number might be small enough that it's worth trying to establish that rigorously for all of them.

[Amir Livne Bar-on]

I didn't think about duality, taking it into account we're down to 440 (and only 8 for order 3, you can use this file and discard everything above Equation410)
unknowns_10_06_d.txt

[Andrés Goens]

note that duality should also be counted as known-true-but-missing-proof, since we're currently still working on that metatheory

[Andrés Goens]

although for the 256 difference I guess we could just manually add the proofs of using duality, we do have enough infrastructure for that already

[Terence Tao]

Even of some of our automated tools end up coming online a little bit too late for the manual completion of the project, they could still be useful for future expansions or variants of the project so certainly worth doing

[Amir Livne Bar-on]

I missed something last night due to a bug in my duality-checking code. There are a few unknown equations with known duals.
18 of the unknowns in the last list are dual to implications disproved by saturation by Vampire, which is confusing to me. 7 unknowns are dual to proven results, out of these 3 follow directly from the dual of All4x4Tables/Refutation726.lean and 2 are counter-examples found with Vampire.
known_duals.txt

[Terence Tao]

That is a little bit odd, if the set of finite magmas one is testing is closed under duality, then the implications it refutes should do so also. Maybe it's because the finite magmas used were generated randomly (so that the dual of the random magma was not tested)?

It would be a little odd if Vampire could resolve one anti-implication but not its dual, but it could be a quirk of how Vampire is implemented, and maybe it's just that out of millions of anti-implications, two of them were so close to the time cutoff that their dual didn't quite make it. Still it would be nice to get to the bottom of this, it is vaguely concerning.

In any event we should then be able to shave off 7 more anti-implications (and add 18 conjectures?) by manually dualizing the Lean proofs associated to the above list. Inching closer to the finish line...

[Amir Livne Bar-on]

I had another bug, where if A is self-dual (A=A') the implications A=>B and A=>B' got merged.
Taking these into account in addition to the 25 above, this is my current list of unique unknown implications:
unknowns_10_07_d.txt

[Terence Tao]

Hmm, I'm not sure how to update the relevant item on README.md (the Oct 6 item in "statistics and data files from a given point in time) in view of this. Would you be able to take a crack at it?

[Amir Livne Bar-on]

Sure, I will document this. Hopefully also with a script to generate the list.

[David Renshaw]

Amir Livne Bar-on said:

I missed something last night due to a bug in my duality-checking code. There are a few unknown equations with known duals.
18 of the unknowns in the last list are dual to implications disproved by saturation by Vampire, which is confusing to me. 7 unknowns are dual to proven results, out of these 3 follow directly from the dual of All4x4Tables/Refutation726.lean and 2 are counter-examples found with Vampire.
known_duals.txt

equational#430 knocks out a chunk of these

[David Renshaw]

looking at the rest now...

[David Renshaw]

equational#431 closes out the last of missing proofs from known_duals.txt. (There are still missing conjectures, i.e. implications that we currently list as "unknown" where the dual has a conjecture.)

[Amir Livne Bar-on]

Wow, this is amazing! It even covers all the tentative confluent equations I found earlier today

[Vlad Tsyrklevich]

I spent a long time being confused today while running some experiments using automated tooling, and it seems the cause why was because equation 5105 is actually equation 5093. 5105 is the similar looking x = y ◇ (y ◇ (y ◇ (y ◇ (z ◇ w)))), e.g. x=y^4(zw) not x=y^3(x(zy))

[Edward van de Meent]

ah... in that case, proving 5105 -> 2 is trivial :upside_down:

[Vlad Tsyrklevich]

These equations in it's neighborhood imply Eq2:

equation 5091 := x = y ◇ (y ◇ (y ◇ (x ◇ (y ◇ z))))
equation 5094 := x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ z))))
equation 5095 := x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ w))))
equation 5098 := x = y ◇ (y ◇ (y ◇ (y ◇ (x ◇ z))))

[Vlad Tsyrklevich]

I've opened equational#714

[Terence Tao]

Oof, it looks like you are right. I'll try to get this fixed. Do you know if any of the other sporadic equations have a similar issue?

[Vlad Tsyrklevich]

No, but that's a good point. Let me check the others

[Vlad Tsyrklevich]

Took a long time to generate order 6 laws (I suspect this can be much faster than it currently is), but I confirmed that other sporadic equations match.

[Terence Tao]

Renumbering complete. equational#715

[Terence Tao]

The CI passed, and I don't see any further appearances of 5105 in the code, but there may be some emergent bugs. For instance I didn't inspect any compressed files that may have the 5105 number encoded in them (but fortunately most of our codebase ignores the sporadic equations, so presumably any such issues will be limited.)