how many explicitly true relations were proved automatically

Stream: Equational

[Ruhollah Majdoddin]

Hello,

I'm new here and mostly interested in machine learning applications for automated theorem provers (ATPs).

I'm curious about roughly how many of the 10,657 explicitly true relations were (or could be) proven by ATP.

From what I've gathered, it seems out of 10,657 explicitly true relations, about 1,775 were proved by (Vampire), 5,574 were identified by MagmaEgg (though many were later found to be implied), and 86 by lean-egg.

I also noticed from Terence Tao's log that all explicitly true relations were established quite early on (by day 14–16). Meaning more than 3,500 of the proofs were found manually in 2 weeks! But is it because these were too easy, or too hard to give to ATPs?

Thanks!

[Terence Tao]

It's a bit hard to give meaningful numbers here because at some point we transitively reduced the set of explicitly true relations to a smaller generating subset, so any statistics reported before that reduction are no longer accurate. We had proposed (in equational#171) something like a daily dump of what the current status of the implication graph was at any given point in time, which would allow for some automated way to answer your question, though we never did get around to it. It's still in principle possible to do with due to the ability to roll back the git repository, but this would require some effort.

The early phase of the project included a "Subgraph" subproject which generated a few dozen implications (mostly trivial in nature). Some of these are still in the codebase as legacy relations, but I think at some point there was a large-scale Vampire run which was able to prove all of the explicitly true relations though.

See also the previous thread #Equational > What are the hardest positive implications for an ATP?

[Ruhollah Majdoddin]

Thank you for the answer. It seems that this wasn't really a challenge for ATPs, as they could easily beat all the explicitly true relations.

So I am curious about the follow up projects—how challenging would they be for ATPs?
Will it be the Hasse diagram but for equations that use magma operations many more times (not just four),
or will it be, as Pace Nielsen suggests, the Euler diagram between Boolean combinations of the identities.

In either case, I assume it would be the job of ATPs for FOL to prove the true relations. Or a more specialized ATP would be a better fit? Even if that ATP needs to be developed.