using z3

Stream: Equational

[David Renshaw]

I proved a new result with z3: equational#291. (The big vampire PR does not include this result.)

[David Renshaw]

Someone should make a script that tries this on all the unresolved results.

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

Nice - if you're willing to post an explicit multiplication table over Fin 8, I'll check whether it disproves any other unknown implications. If so, it might be worth adding the table to the manually-curated set in All4x4Tables (which is a major misnomer at this point, we have lots of interesting tables up to 9x9 there).

[Nicholas Carlini]

+1 to renaming this something more sensible now that it's not just 4x4.

It may be worth trying to pin down some kind of "API" so that as we collect cases where some equations hold true we can automatically gather the refutations for equations where it's false

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

@Nicholas Carlini : Indeed. There are some tools in finite_magma_tools which do most of what's required (auto-testing equations in multiplication tables, writing output, etc.) but they'll require a few changes before they can be integrated into such a pipeline.

The bandwidth I can dedicate to this project from next week on is likely going to be much lower, but if somebody creates an issue and takes it up, I'll be happy to assist.

[Terence Tao]

equational#180 is basically the issue for this. I'll link back to this thread to coordinate discussion. As I wrote in a comment at equational#294, this is my vision for the interface:

"Ultimately one could imagine a web interface where one could upload (in some standard format) a multiplication table, the tool displays all the equations it satisfies, checks if it creates any new refutations, and if so it accepts the table and adds it to some standard directory from which the refutations are generated. There may be a few thousand finite magma refutations left out there, so this might be worthwhile."

[David Renshaw]

Zoltan A. Kocsis (Z.A.K.) said:

Nice - if you're willing to post an explicit multiplication table over Fin 8, I'll check whether it disproves any other unknown implications. If so, it might be worth adding the table to the manually-curated set in All4x4Tables (which is a major misnomer at this point, we have lots of interesting tables up to 9x9 there).

#eval (List.range 8).map (fun ii ↦ (List.range 8).map (fun jj ↦ f_834_10 ii jj)))

yields

[[4, 1, 0, 0, 1, 0, 4, 1],
 [3, 1, 1, 2, 2, 1, 1, 1],
 [2, 2, 5, 6, 2, 6, 2, 2],
 [3, 2, 5, 2, 3, 3, 3, 3],
 [3, 3, 4, 4, 3, 4, 4, 3],
 [5, 5, 6, 5, 5, 0, 7, 0],
 [4, 6, 6, 6, 6, 0, 0, 0],
 [4, 7, 7, 7, 1, 4, 4, 1]]

[David Renshaw]

equational#297

[Nicholas Carlini]

As a comment on the "All4x4Tables", I'm about 20% of the way through all commutative 5x5s and so far can prove nothing new that wasn't already shown

[Terence Tao]

Thanks for the update. It seems that the implications around the commutative law are actually quite close to complete already, so I guess there wasn't that much low hanging fruit left here. Still, even negative results are good to know.

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

@Nicholas Carlini I suspect there are very few (if any) new 5x5 counterexamples left in general, for the following reasons:

• @Daniel Weber's vampire runs generated a lot of new 10x10 counterexamples, but I don't recall seeing any 5x5s from browsing the files. (might be a config artifact, see below)

• There are relatively few equations in the dataset which cannot be satisfied in nontrivial cancellative monoids, and they're generally of the form x=f(x,...). I've given these some special manual attention while playing interactively with constraint solvers, but could not find any new 5x5s this way either. In contrast I find 6x6s occasionally.

Unsuccessful runs can be disappointing (ask me how I know), but it'll be all the more interesting if the 5x5 commutative search does find something: it'll be a special little magma indeed.

It might be too late now, but it's worth keeping track of equations which only have nxn counterexamples for n>5 among the cancellative magmas, but have 5x5 noncancellative counterexamples!

[Daniel Weber]

I think the reason my run generated mostly 10x10 counterexamples is because that's the size Vampire uses by default, or something along those lines - I don't think that's an argument for there not being relevant smaller magmas

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

Daniel Weber said:

I think the reason my run generated mostly 10x10 counterexamples is because that's the size Vampire uses by default, or something along those lines - I don't think that's an argument for there not being relevant smaller magmas

Okay, that's important and good to know! I'm all the more excited about the search finding some good 5x5s.

Can you adjust that n=10if you do any future runs? Smaller counterexamples are a lot better when you have many variables and need to do exhaustive checks. The compiled Haskell has so far been fast enough to handle them, but Lean might struggle.

[Daniel Weber]

I tried a bit to adjust that, but I couldn't figure out how to

[Daniel Weber]

I looked at it a bit harder, and I think I managed to do it now

[David Renshaw]

Got another one: equational#308

[David Renshaw]

My process here is:

1. Open the output of outcomes_to_image.py in GIMP and find a black pixel that looks likely to resolve to red.
2. Plug it in to z3.

I tried it twice so far, and in both cases it succeeded.

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

That's clever! :) This one resolves a lot of antiimplications too!

[Terence Tao]

Is @Pace Nielsen 's 5 x 5 magma from #Equational > visualization of graph closure in the list of finite magmas yet?

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

@Terence Tao I am working on a major commit which should add a lot of stragglers to All4x4Tables, I'll include it there.

[Terence Tao]

If there is some way to add comments to that list of tables it might be nice to briefly mention where some of these magmas come from

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

There is a way -- all lines that don't start with Table ... or Proves ... (or Magma ..., Satisfies ..., Refutes ... in the plans) are ignored by the tools, so we can add a Provenance ... line.

But I'll also include them as separate files, so it'll be possible to git blame them and get proper context.