A magma of order < 13 - for Equation2531?

Stream: Equational

[Zoltan A. Kocsis (Z.A.K.)]

In PR #330 I give a 13x13 counterexample showing that the dual pair 1076/2531 do not imply a bunch of stuff. In particular, it shows that 2531 does not imply 1075.

I'm very happy about this, since this pair of dual equations had by far the highest unknown count among those equations that are not implied by anything else.

The multiplication table is below.

 0, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12, 1
 2, 1,11, 7, 9, 4, 8, 0, 3,12, 6, 5,10
 3,11, 2,12, 8,10, 5, 9, 0, 4, 1, 7, 6
 4, 7,12, 3, 1, 9,11, 6,10, 0, 5, 2, 8
 5, 9, 8, 1, 4, 2,10,12, 7,11, 0, 6, 3
 6, 4,10, 9, 2, 5, 3,11, 1, 8,12, 0, 7
 7, 8, 5,11,10, 3, 6, 4,12, 2, 9, 1, 0
 8, 0, 9, 6,12,11, 4, 7, 5, 1, 3,10, 2
 9, 3, 0,10, 7, 1,12, 5, 8, 6, 2, 4,11
10,12, 4, 0,11, 8, 2, 1, 6, 9, 7, 3, 5
11, 6, 1, 5, 0,12, 9, 3, 2, 7,10, 8, 4
12, 5, 7, 2, 6, 0, 1,10, 4, 3, 8,11, 9
 1,10, 6, 8, 3, 7, 0, 2,11, 5, 4, 9,12

As you can see, it's commutative. There are no smaller commutative examples.
But I find 13x13 quite large for a small magma. Maybe there's a smaller, non-commutative example? If somebody wants to play around with Vampire, I think it could probably answer this question.

[Terence Tao]

I wonder if it is worth recording (ideally in the blueprint) the process for discovering these examples, as this could be valuable knowledge for any future researcher wanting to do similar counterexample hunting. To what extent is this computer assisted?

[Zoltan A. Kocsis (Z.A.K.)]

I think others will document much better strategies. My method is very much like mining: the computer digs through large quantities of rock, and I try to direct it to veins that might have precious material.

When I want to disprove the implication X -> Y, I usually use Prover9 and Mace4 in tandem. I set a small search space, typically up to 6x6 optables. Mace4 can quickly cover 2x2, 3x3, but starts slowing down as it reaches 5x5 or 6x6 (depending on the equations X and Y, this could happen earlier or later).

Next, I introduce additional conditions that might be relevant, such as requiring the structure to have some good endomorphism (perhaps relevant to the equation), or that the magma operation preserves some added structure (e.g., a digraph, partial order, or another algebraic operation). Cancellativity itself started out as one of these, but it worked often enough that I decided to do an exhaustive search, which eventually led to the 5x5 enumeration.

As I add assumptions, I monitor two things:

1. Can Prover9 prove the implication X -> Y given my additional assumptions? If yes, there can't be a counterexample like this, so I move on to a weaker assumption.
2. How quickly does Mace4 exhaust the search space for different sizes (it helpfully reports when it moves on from 3x3 to 4x4 etc.).

The goal is to set up a scenario where:

1. Prover9 cannot find a proof of X -> Y after some reasonable time (checking the proof trace helps see if it's even trying anything useful);
2. But Mace4 quickly handles the small search spaces.

When both conditions hold, I crank the table size N up to a large value, and usually, a counterexample appears shortly after. This is how I got the 13x13 example: when I tried commutativity, Mace4 started churning through the small tables really fast, but Prover9 was not finding a proof. I increased N, and the 13x13 table appeared within a second (which is unusually fast).

[Zoltan A. Kocsis (Z.A.K.)]

I think, in general, we're throwing away quite a lot of information that we could in principle extract from failed searches: nobody ever sees which partially-filled matrices Mace4 explored, and what kinds of contradictions it gets into that force it to backtrack. Looking at timings is really a (somewhat poor) proxy.

I think in lots of cases where an implication is true, one could get a good idea of how a proof will go based on the abandoned partial optables.

[Terence Tao]

This is a fascinating synergy between automated tooling and human direction!

[Michael Bucko]

(deleted)

[Michael Bucko]

Perhaps we could write a tool that outsources that process to a language model that uses Prover9, Mace4, and Lean's LSP? We would not fully outsource the process - it'd still be guided by a simpler pseudocode. Does that make sense?

[Michael Bucko]

I just wrote it in Python (it currently takes the argument from the command line and then processes it with Lean by creating a temp file first (a subprocess)).

https://github.com/riccitensor/mathplatform/

Prover9 and Mace4 are commented out atm, but can be added.

Currently, GPT-3.5 is the main LLM, but Claude (or a newer GPT) can be added.

Given its lean structure, it could easily be integrated into Equational, into our current workflows, or even agentic workflows could be created on top of it. It could essentially make decisions about which tools it needs and for what, and, esp. with GPT-O1, it could help us automate search (and more).

Workflows like the one Zoltan mentioned could be integrated into the existing codebase through agents built using this tool.