Writing the paper

Stream: Equational

[Terence Tao]

Now that we have completed our primary goal, the next major goal is to finish the writing of the draft paper. (One can of course still pursue additional spinoff projects, as we have already been doing for instance with the finite magmas spinoff, or make technical improvements to the codebase; but in my mind the "official" part of the project will wrap up once the paper is written, submitted, revised, accepted and published.)

We already have several issues claimed equational#873 equational#922 equational#926 equational#956 to contribute chapters or subsections to the draft that are still outstanding. Perhaps this thread can be used for the contributors who had claimed these sections to report on their status.

One of the writing issues, equational#924 (writing a section reporting on the finite magma implication spinoff project), remains unclaimed (a stub exists in the draft at Section 8). A volunteer to claim this section also would be greatly appreciated!

I plan to go through the draft later today to update it and identify any further issues to formally make (based on several boldface comments currently in the draft). A lot of it is in decent shape though, so I think once we have the contributed chapters we can move into the proofreading and polishing stage. (But if anyone has any suggestions for the global structure of the paper, this thread would be a good place to discuss them.)

If any contributors wish to register themselves as a participant or co-author of the project but has not yet made a contributor PR listing your contributions, this would be a good time to do so. Contributors can also update their contact and contribution details in Appendix B of the paper.

An obvious journal for this paper, by the way, would be the newly formed Annals of Formalized Mathematics, but this would also be a good time to discuss any other possible options.

[Shreyas Srinivas]

I guess for most junior people in academia, an established venue would help more than a new one. But I don’t know much about math journals so I can’t really suggest alternatives

[Terence Tao]

I've gone through the paper and done some cleanup. For instance, I've removed the "statistics" section as we don't really have much to report here (but instead sprinkled some more stats about the implication graph elsewhere in the paper), and also shortened the "Author contributions" section since we are using the contributions.md file as our main source here. (But we should include contact information and affiliation in the main paper still; if you are listed as an author but have not entered in this information, feel free to submit a PR or else DM me with the required details.)

The most significant content I added was in the "conclusions" section (Section 13), where I proposed some lessons to draw from the project, and some future directions. This is very much a tentative draft for this section, and I very much welcome more input to weigh in on what lessons to draw from this project. There may be things that I omitted, or misrepresented, or perhaps are not worth saying, so any feedback would be encouraged here.

I also wrote something for Section 3 (formal foundations), though I was a little unsure about some of the backend stuff (e.g., how we ended up implementing laws vs equations), so some scrutiny and corrections here would also be welcome.

One section that is still completely missing is Section 12 (data management), which is something we really haven't talked about. Presumably the Github repository will be our primary data repository going forward. The actual data of our project, particularly the implication graph, can be accessed from Equation Explorer, though I don't think we quite have a way of converting an arbitrary edge in the graph to an actual Lean theorem yet. Is there anything we could do to make the data we have more accessible that doesn't require an enormous amount of additional effort?

[Mario Carneiro]

The actual data of our project, particularly the implication graph, can be accessed from Equation Explorer, though I don't think we quite have a way of converting an arbitrary edge in the graph to an actual Lean theorem yet.

That sounds like a relatively easy task (a lot easier than constructing the full implication graph in lean)

[Mario Carneiro]

the easiest implementation I can think of is to just have explain_implication.py produce json output and then have a lean tactic use that to figure out which theorems to string together

[Mario Carneiro]

oh this is fun, I proved false using explain_implication.py

$ scripts/explain_implication.py Equation2 Equation2
Found contradiction!

Equation2 => Equation2  (tautology)
Equation374794  has a model that does not satisfy  Equation2
    InfModel.Equation374794_not_implies_Equation2  in  InfModel.lean
Equation374794 => Equation2
    InfModel.Finite.Equation374794_implies_Equation2  in  InfModel.lean

[Terence Tao]

Oh, is there some bug in confusing the finite implications with the infinite ones?

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

Re data management: last year, I believe somebody mentioned a specific science data repository which could host a long-term archive copy of the repo as it is on the date of acceptance.

At the moment my Zulip-fu is not strong enough to find it, though. Does anybody remember who/what this was?

[Alex Meiburg]

Zenodo, probably? It's a repository with DOIs (so, good long term archival) that's particularly built to preserve code or datasets.

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

Indeed, and MathBases, mentioned here

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

Thanks @Alex Meiburg !

[Terence Tao]

We are listed on MathBases at https://mathbases.org/d/equational-theories but it is just a small amount of metadata, the repository itself is not hosted there.

[Terence Tao]

Submitting a static copy of the repo to Zenodo upon acceptance of the paper makes sense to me.

[Andrés Goens]

I also wrote something for Section 3 (formal foundations), though I was a little unsure about some of the backend stuff (e.g., how we ended up implementing laws vs equations), so some scrutiny and corrections here would also be welcome.

Happy to give that one a shot (and send a PR)!

[Terence Tao]

Great! I've opened equational#1178 to officially make this an issue for you to claim. EDIT: Oh, I see you already submitted the PR, so I'll close this issue as completed.

[Douglas McNeil]

I have a branch with 80% of https://github.com/teorth/equational_theories/issues/956 done which I worked on last year :sweat_smile: -- I don't think there's much left to do except hunting down some refs, so I'll make time over the next while.

[Shreyas Srinivas]

I am drafting the section on how we managed this project. I will be making commits in small chunks every now and then. There are some TODOs in the middle, mostly about looking for citations or notes to double check a point.

1. If you have any suggestions, especially about the TODOs, feel free to comment on the PR, even as I draft it.
2. Comments about the broader thrust of the content would be more helpful once the draft is complete, since I am likely to make non trivial changes to the content anyway.

[Shreyas Srinivas]

The relevant PR is here: https://github.com/teorth/equational_theories/pull/1038

[Shreyas Srinivas]

Could we shorten the paper title a bit? It seems rather long.

[Shreyas Srinivas]

The current subtitle sounds like a sentence that belongs in the abstract.

[Alex Meiburg]

I think it's a matter of what you find to be the most exciting aspect of the project. In my opinion, the actual material mathematical results (while neat and interesting!) are not likely to be of particularly broad or deep interest; the meta-level fact that the project could be distributed and verified as it went along (and the distribution relied on verification, in the sense that it meant we didn't have to 'trust' each other) will maybe be the most intriguing part of the project. Hence why the paper also goes into pretty substantial detail about the discovery process, which is typically glossed over in a math paper.

[Shreyas Srinivas]

I get what you mean, but I think the subtitle could at least be shortened.

[Shreyas Srinivas]

We don't need to single out lean or github in the subtitle at the very least. Github, while immensely valuable, is definitely not ireplaceable in the project. We could have accomplished everything just the same with bitbucket, trello, gitlab etc.

[Shreyas Srinivas]

Maybe "The Equational Theories Project : Mathematical Research at Scale"

[Shreyas Srinivas]

Or "The Equational Theories Project : Scaling Mathematical Collaboration"

[Terence Tao]

These work for me. Any other proposals? I can set up a poll.

[Pietro Monticone]

Maybe something that feels slightly more "complete" like The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale ?

[Shreyas Srinivas]

I don’t think we need to make it so qualified. A slightly shorter title that gets the gist across is better

[Terence Tao]

/poll What is your preferred title for the paper?
The Equational Theories Project: Using Lean and GitHub to complete an implication graph in universal algebra
The Equational Theories Project: Mathematical Research at Scale
The Equational Theories Project: Scaling Mathematical Collaboration
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Other

[Terence Tao]

It's far from a consensus, but I have gone ahead and implemented the plurality title choice of "The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale"

[Jose Brox]

Terence Tao ha dicho:

We already have several issues claimed equational#873 equational#922 equational#926 equational#956 to contribute chapters or subsections to the draft that are still outstanding. Perhaps this thread can be used for the contributors who had claimed these sections to report on their status.

As contributor to equational#922, I must say I have yet to start writing :sweat_smile: I have some commitments to students right now that I must fulfill first, but once I start writing, it shouldn't take too long.

[Shreyas Srinivas]

Do we have the minted latex package already in the source? I would like to use it to insert lean4 snippets

[Terence Tao]

I don't think so, but feel free to add it if it is not there

[Martin Dvořák]

Do we want to submit the paper to CPP 2026?
https://popl26.sigplan.org/home/CPP-2026
The deadline is 2025-09-05 for abstracts and 2025-09-12 for papers.

Unfortunately, they allow only 12 pages (appendices are possible tho).
Also, I don't know whether it is feasible for our paper to undergo a double-blind reviewing process.

[Kevin Buzzard]

It's not your problem as an author to worry about a double-blind reviewing process, so this shouldn't be a consideration.

[Kevin Buzzard]

However my impression is that cutting it down to 12 pages might involve some big (and in fact unreasonable) sacrifices.

[Shreyas Srinivas]

In most computer science conferences, double blindedness means that you shouldn’t go out of the way to advertise the authors to the reviewers. I don’t know if the PL community has moved on to a stronger standard

[Shreyas Srinivas]

But basically putting stuff on arxiv is fine

[Shreyas Srinivas]

If the reviewers find out without intent that is also unavoidable and therefore fine

[Shreyas Srinivas]

Also I know this is specific to some communities but huge appendices are not uncommon in some CS conferences these days. Entire papers exist in appendices and the “main” paper is an extended abstract and overview of results. Again, I am not sure if this flies at CPP.

Alternatively, we could publish a conference and a journal version. This will count as one publication unit within CS. I don’t know how this changes in math.

One point to note is that the ACmart class with 10pt font is quite dense compared to what we are using right now.

[Terence Tao]

Given the slow pace of writing the primary paper, I am not optimistic about the ability to produce a second paper in a reasonable timeframe, and I am not sure what additional content it could have that would not already be suitable for the primary paper (or for supplemental material such as the blueprint). I could imagine the ETP data being a component of some future research project that could go into a venue like this, but this might be accomplished by some other group of collaborators than the ones for the primary objective of the project.

[Shreyas Srinivas]

The basic reason for slow progress is that I think for a lot of us, academic and work life caught up

[Shreyas Srinivas]

We were able to give a lot of time to the project in the initial months, but the resultant backlog eventually caught up with many of us

[Douglas McNeil]

Are we close enough that it's worth doing some copyediting? There are some minor typos (4694 vs. 4964) and inconsistent use of hyphenation, some cases where diacritics are lost from names, etc. We'll have to do it again later anyhow, but some of these are going to need to be fixed regardless.

I have to admit it was an AI that spotted the 4964 typo in the third sentence of the paper.. :sweat_smile:

[Terence Tao]

Sure, feel free to submit PRs for these sorts of corrections.

[Bruno Le Floch]

I'm wondering about some chapters of the blueprint. There are some non-trivial results hidden there, at least some about specific laws such as weak central groupoids, or magma cohomology, or the spectrum (not quite yet in the blueprint). If the blueprint is submitted as supplemental material to the main publication, these more detailed results would no longer be publishable since they would already appear as part of a publication, but at the same time they would be pretty hard for people to find and reference.

[Terence Tao]

I should get around to putting a CITATION.cff for the equational theories github repository, so that one can at least reference through that

[Terence Tao]

OK, we now have a CITATION.cff : equational#1265

[Shreyas Srinivas]

To all authors : Please check for underflow and overflow warnings. Please eliminate them in your PRs

[Terence Tao]

Are you planning to fix the errors that you find in other sections in your own PR? I can go through the entire paper to address these, but I want to avoid merge conflicts.

[Shreyas Srinivas]

I don’t think these will be merge conflicts since they are in separate files

[Terence Tao]

Right, the question is whether you wish to fix the errors in these other files, or if you would like me to do so. If we both do so then there could be a merge conflict.

[Shreyas Srinivas]

I prefer these fixes to be a separate PR

[Shreyas Srinivas]

Since they touch different files, there is no worry of merge conflicts

[Shreyas Srinivas]

So I don’t mind it if you make a pass through the paper. If any merge conflict does arise, I should be able to handle it.

[Terence Tao]

OK, then I will go through the paper now.

[Douglas McNeil]

What's the best procedure to comment on random bits of the paper that might need some edits, but will need someone else to chime in?

For example:

We also define the order of a word $w \in \Magma_X$ to be the number of occurrences of $\op$ in the word, thus letters in $X$ are of order $0$, and the order of $w_1 \op w_2$ is the sum of the orders of $w_1, w_2$.

Doesn't that need to be 1+order(w_1)+order(w_2)?

And

In fact, since these equations preserve the space of homogeneous polynomials of a fixed degree, one can use linear algebra to locate an example that is a homogeneous polynomial; one explicit choice is $f(x,y) = y^5 +xy^4 + x^2y^3 +3x^3 y^2 + 3x^4 y_1$.

where y_1 must be a typo, etc.

[Terence Tao]

This is as good a place as any (the Github issues page would also work). I've fixed the two typos you mentioned.

[Shreyas Srinivas]

Just pushed a conceptual overview of the project contribution process with a couple of figures. I didn't rehash all of CONTRIBUTING.md

[Shreyas Srinivas]

what remains is describing the importance of maintenance and scalability issues, and shortening the description of the trust issues with ITPs (adding a reference to Mario's explanation from the external checkers book)

[Martin Dvořák]

/poll Where do we want to submit the paper? [This is not a referendum. I'm just curious about what people think.]
Annals of Formalized Mathematics
Journal of Automated Reasoning
A different journal?
A conference?

[Terence Tao]

I put down a vote for AoFM as it is a newer journal and I felt this would be a way to support it, but if there is a majority preference for JoAR instead I'm fine with that one as well.

[Douglas McNeil]

More misc comments!

Possible typo?

One such example is the refutation $\Eq{1485} \vdash \Eq{151}$, which we discuss further in \Cref{twisting-sec} below.

E1485⊬E151 , no?

---

Maybe typo, maybe confusion on my part: in the explanation of the greedy method, we write:

• Case 4: x, y, x ⋄′ y, y ⋄′ (x ⋄′ y) != c: this case is covered by Rule 3 for ⋄.

I'm not sure how rule 3 applies here. I would have thought something more like

“Case 4: x, y, x ⋄' y, y ⋄' (x ⋄' y) != c. In this case ⋄'=⋄ on all pairs, so the claim reduces to Rule 1 for ⋄, which holds by the induction hypothesis.”

and the appeal is to rule 1, not 3.

---

When we introduce the twisting semigroup in 5.4, with example 5.11, does that equation really follow from E1485 with TU=UT & T^2=E^3? How do we kill the TU on the LHS after x->TUx? We haven't assumed TU=1 yet, and we're working with endomorphisms, not auto. Could probably use some more explanation.

[Terence Tao]

Thanks! I have fixed the typos. One should indeed assume that TU=UT=1, not just TU=UT, here.

[Douglas McNeil]

Could someone review example 5.2, the counterexample to E1286->E3? I'm having two separate arithmetic challenges with it (the variety calculation itself and the second p,a,b example.)

[Terence Tao]

Looks like there was a spurious "+a" term in the first equation defining the variety; I've fixed that now.

[Douglas McNeil]

Good, that matches my calc too. For the second issue, I don't see how p,a,b=(7,6,2) works here. 6+2=8=1 mod 7, so a+b=1, and won't E3 be satisfied? I think that combination satisfies E1286, but won't work as a witness.

[Terence Tao]

Ah, you're right; the p=7 model is the smallest nontrivial model for 1286 but it is indeed idempotent (obeys E3). This was not properly reported in the commentary for 1286 so I am changing that also.

[Douglas McNeil]

On prop 5.16, E1659 =/> E4315, I'm confused.

A minor point is that I think in (1, 0) != ((0, 0) ⋄′ (1, 0)) ⋄′ (((1, 0) ⋄′ (1, 0)) ⋄ (1, t)) we'll need the last ⋄ to be ⋄' as well.

A more major one is that I'm not sure the proof works as written, in that the override seems to violate 1659. Unfortunately this requires me to trust my arithmetic, a fool's game. :wink:

G has carrier Z/2Z and M has carrier Z. If we set "(0, 0) ⋄′ (1, t) = (0, 0) for all t ∈ Z" as the paper says, then x=(0,0), y=(1,-1), and z=(1,0) gives LHS=(0,0) and RHS of (1,0), breaking E1659, so it can't witness the refutation.

It looks to me like both this model and the parity model from the blueprint only work for N, not Z, and we should adjust the text accordingly, both the carrier and the examples.

If so, the wording in the blueprint that "At this point one might as well truncate the model to N" seems a little misleading, because it's not like things were working over Z and we dropped down to N for simplicity. I seem to see lots of E1659 violations in Z.

As always, caveat lector!

[Terence Tao]

Thanks, I have reworded the text in the paper and blueprint accordingly.

[Douglas McNeil]

In the proof of lemma 6.9, E854->E378, I think we set y=S^2 x when we meant to set z=S^2 x in this line:

$$x = x \op f(x,S^2 x,x) = x \op S(x \op S^2 x) = x \op S(x \op f(x,x,x)) = x \op Sx.$$

Otherwise I can't see how the f()->S() step goes, but if it's meant to be y:=x, z:=S^2 x, we get
f(x,x,S^2 x) = ((x∗S^2 x)∗(x∗S^2 x)) = S(x *S^2 x) as needed.

[Terence Tao]

Fixed, thanks!

[Douglas McNeil]

So I'm trying to follow the "canonization" section. A lot of the rewriting-related stuff still feels like magic to me, so maybe I'm just missing the sleight-of-hand. :wink:

My current problem is that our definition 6.6 of canonizer seems so weak! All we have is that C is computable and that w_1 ~=_E w_2 => C(w_1) = C(w_2). So it's kind of a class labeller. Most other references I've found involve soundness, idempotence, and compositional assumptions. It seems like a trivial canonizer C(w)=x would match our definition, and if that's true we're clearly limited in what we can conclude.

Note that we can then take the image of C and endow it with a magma structure simply by
taking w1 ⋄ w2 := C(w1 ⋄M_X w2 ). This magma refutes E ′ if C sends the left-hand-side and the right-hand-side of E′ to distinct elements of MX .

At this point all C has is computability and class invariance. How do we know this image actually models E?

[Terence Tao]

@Cody Roux I think you wrote this part of the paper, would you be able to weigh in on this?

[Cody Roux]

@Terence Tao @Douglas McNeil Sure! I was somewhat mystified as well, so perhaps, barring mistakes on my part, we can build a better explanation for the text.

First, note that in

$$w_1\simeq_E w_2\Rightarrow C(w_1) = C(w_2)$$

I mean "for any provable equation from E", rather than just

$$E = \{(w_1, w_2)\}$$

Generally, you'd like at least one additional property from your canonizer, namely

$$C(w)\simeq_E w$$

which gives you

$$w_1 \simeq_E w_2 \Leftrightarrow C(w_1) = C(w_2)$$

as expected. But actually this is stronger than what we want, which is just to refute implications! And indeed the Lean proofs do not prove this extra property, at least directly.

I'm not sure I found a very standard definition of a canonizer, though I guess a case can be made that it includes this second condition, in which case we need to find another term, maybe "weak canonizer", though I used that elsewhere for something else.

At this point all C has is computability and class invariance. How do we know this image actually models E?

This is the bit I'm actually not sure about. Actually, no, I'm sure this is wrong.

In the code they actually have the additional idempotence hypothesis, but that's also not enough. They just prove each special case, but there the canonizer is defined as in definition 6.7, so everything works out: C_R is idempotent and a morphism to the magma defined as above. The trick is that R actually satisfies some pretty strong conditions (the subterm and non-overlap stuff). This makes C_R idempotent but also respect substitutions on the image.

I should note that we don't actually need this, since if C sends E- equal words to distinct terms, it's definitely a matching invariant (in the sense of 6.2) like mentioned in the previous sentence, and so we don't actually need this to be a magma satisfying E in the rest of the paragraph.

Still I'm annoyed at the mistake, and the lean code does prove that each instance is a model for the given magmas. Maybe I can explain why it holds in this case.

(As an aside, the matching invariant mentioned in Proposition 6.1 is the universal invariant).

Second sidenote: I notice that in the following paragraph they use

$$x \sim_E y$$

instead of

$$x \simeq_E y$$

Should I change my notation?

[Douglas McNeil]

Let's see if I'm following..

So we use the class invariant C just to show non-derivability, without insisting that im C models E. We're only appealing to Birkhoff completeness (magic! :magic_wand:)

I guess the text as written never actually claims it's an explicit refuting model for E/E', but "this magma refutes" does make it sound like that.. even though we really just mean "We’ll use a computable, $E$-invariant $C$ purely as a proof-theoretic refutation: if $C(\text{LHS}_{E'})\neq C(\text{RHS}_{E'})$, then $E\nvdash E'$ (by Birkhoff completeness)" or something.

To answer my earlier concern, the trivial mapping to a constant element is indeed a valid "canonizer" by 6.6, it just doesn't have any separating power as a refutation witness, because by construction there's never going to be anything different on the two sides. So it's not a problem that it's valid, nobody ever promised every canonizer would have much proving power! I guess that makes sense too.

By way of contrast, for a explicit countermodel/model-theoretical refutation we'd need a compositional C to ensure im C models E, and 6.6 doesn't suffice. I'm not sure whether even 6.7 does.. I've gone back and forth on whether I think 6.7 implies idempotency on its own. Currently "yes, via induction on subwords because of the weakly collapsing property", but I thought I had a counterexample a while ago so I was wrong at least once! which is one way to get from CR​(u⋄v)=R(CR​(u)⋄CR​(v)) to CR​(u⋄v)=CR​(CR​(u)⋄CR​(v)) and get a model of E.

Does that make sense?

I think this section could use a few sentences to clarify the storyline.

[Cody Roux]

You're correct on all points! I did think the thing I described was indeed a model, but it's not in general, so I'll make a PR at least fixing that tomorrow.

6.7 is enough for idempotency, at least in the sense that if R is collapsing then C_R is idempotent, that's proven in Confluence.lean. The collapsing condition is quite strong. It's also quite useful in magmas, I think, since there's only one function symbol/operation.

I proved 6.8 in Lean, because I don't trust my paper proofs anymore (if I ever did). I do actually think this is sufficient for being a model. At any rate one can always reconstruct such a model from the matching invariant one way or another.

I'll prove it tomorrow as well if I have time, otherwise I'll just delete the offending sentence and leave it at that, unless there's an objection.

[Douglas McNeil]

@Cody Roux : thanks!

While I'm browsing metatheorems.tex, we say

(1) We work in the free group $\Magma_X$ on two generators $X = \{\x,\y\}$. Free group, or free magma?

(2) We have two references to M_X which should probably be Magma_X.

I think I'm slowly running out of typos.. :upside_down:

[Cody Roux]

You're a hero!

[Terence Tao]

Perhaps it is time for an update from the various people involved in writing the paper to report on how they are progressing? I think it would be good to wrap things up while we still have reasonably fresh memories of the project.

[Shreyas Srinivas]

I’ll wrap up in the next 36 hours

[Shreyas Srinivas]

I am almost done in any case. Just need to go over the notes and check if I covered all the points and add them.

[Shreyas Srinivas]

Apologies for the delay, it shall be done soon.

[Cody Roux]

Finally fixed the typos caught by @Douglas McNeil , things should be done on my side AFAIK.

[Bruno Le Floch]

About our work on various types of spectra of equations, I will write (hopefully next week) something about the full spectrum problem (for the paper). Possibly also something for the blueprint, but I am not sure what will make sense to write there.

The full discussion of counting magmas etc would be better placed in a separate publication I would say, as it is only loosely connected to the implication graph. (However, we did make heavy use of the implication graph to know the finite equivalence classes, and to directly know that some equations were gaseous as soon as stronger equations were shown to be.) Does that make sense?

[Shreyas Srinivas]

I think it could easily be an appendix of the paper or even a section

[Terence Tao]

The paper is already somewhat long and sprawling, and is only intended to be a sampler of the results we have rather than a comprehensive list. So we can mention this spinoff and say that details will appear elsewhere (either in the blueprint, or in some completely separate document).

The blueprint can be held to much more relaxed standards of writing than the paper which is to be submitted to a research journal, in particular a minimally organized and only partially complete discussion is I think fine there, especially given that it can always be updated later (one can insert "TODO"s etc. as needed if one wishes to emphasize the incomplete nature).

[Bruno Le Floch]

Reading the conclusion section of the paper, I notice that E5093 is misquoted here (and in Appendix A), it should be x = y ◇ (y ◇ (y ◇ (x ◇ (z ◇ y)))) or in TeX code \x \formaleq \y \op (\y \op (\y \op (\x \op (\z \op \y)))). The currently quoted equation is E11232 x = y ◇ ((y ◇ (y ◇ x)) ◇ (z ◇ y)). I don't have access to Kisielewicz' paper https://doi.org/10.1007/s000120050057 to see if he also discusses that equation. If anyone has access I'd be interested, if only to record all equation numbers in the commentary.

Another confusion I have about the conclusion is the usage of "surjunctive" for the property that « maps from M to itself that are surjective are necessarily injective ». Firstly, up to axiom of choice subtleties, this property is equivalent to finiteness. It only stops being so if we restrict to maps that are built from the magma operation somehow. This may be related to the usual definition of surjunctivity for groups, which appears to involve cellular automata, but I don't understand enough to fix this. (Incidentally it is possible that the implications 3342⇒3522 and 3342⇒4118 may have surjunctive counterexamples despite holding for all finite magmas, since we use stronger properties than just surjectivity⇔injectivity.)

[Terence Tao]

Thanks! On looking at the original paper of Kisielewicz it looks like this was a typo and 5093 should be used instead:

image.png

I've fixed the manuscript accordingly. As for surjunctivity, the intention is to restrict attention to definable maps as you say; I've modified the wording to make this clearer.

[Terence Tao]

Any further updates from section writers? Hopefully we are close to the finish line...

[Shreyas Srinivas]

I’ll have time to do my final pass tomorrow

[Shreyas Srinivas]

Pushed many edits today. A little bit remains.

[Shreyas Srinivas]

I am briefl writing about the blueprint. But isn’t the standard blueprint already described in detail in other ITP papers?

[Shreyas Srinivas]

I don’t want to say anything beyond “we use the blueprint to tool to organise and track our effort. Unlike other projects, this project did not have a small number of specific top level goals but ca. 22 million goals of a similar sort, which were resolved in wildly different ways. Thus unlike projects where we start with a blueprint to guide our progress, we found ourselves guided by ATP explorations. The blueprint followed these discoveries and formalisation came afterwards, or in tandem”

[Shreyas Srinivas]

We can quote an example here maybe

[Shreyas Srinivas]

Also, do we have a guideline for citing the daily log? Currently I am citing the repository and mentioning the daily log entry in the optional argument . Adding a separation citation bibtex entry for the logs feels like overcitation

[Shreyas Srinivas]

I have removed references to the log. A first draft is ready for review (https://github.com/teorth/equational_theories/pull/1038). I could merge this PR and then subsequent PRs could edit this section

[Shreyas Srinivas]

I think the engineering issues which are solved by duality and transitive closure should be mentioned in the metatheory section to avoid redundancy

[Terence Tao]

I think this level of mention of the blueprint is fine - it is a component of the project, but not a central one like it is in formalization projects, still it is worth making the point that blueprinting can be useful as a secondary tool.

I think the github repository is a good enough reference for all material hosted there (blueprint, log, etc.), and that specific URLs are not necessary.

[Terence Tao]

Overall looks good! A lot of things stated that may be "obvious" to participants inside the project, but would be valuable information for people interested in starting a collaborative project from no starting experience. I added some mostly grammatical comments.

[Shreyas Srinivas]

I think I have responded to almost all of the review comments. If there are no further review comments, I will merge this PR tonight so the content appears on the main paper pdf

[Shreyas Srinivas]

We can still make changes in subsequent PRs

[Shreyas Srinivas]

There were no comments. I have merged. This also saves any further merge conflicts. In sometime the new version of the paper should show up on the webpage. Feedback is definitely welcome.

[Cody Roux]

Excellent work @Shreyas Srinivas !

[Bruno Le Floch]

Maybe we could add to the paper the following Hasse diagram of all implications between (equivalence classes of) laws of order 0,1,2: Hasse_low_eqs.png (sources Hasse_low_eqs.py and Hasse_low_eqs.tex giving Hasse_low_eqs.pdf). It is a reorganized version of the graph produced by Graphiti,
Hasse_low_eqs_Graphiti.png, with some effort to keep duality symmetry manifest (self-dual equation ids are underlined) and organizing according to how the asymptotic number N(n) of magmas of size n behaves, e.g. log(N(n))=(1-p)n^2 log(n) for gases.

[Shreyas Srinivas]

Feel free to add it in your PR. It looks good

[Terence Tao]

Nice! My only suggestion is to somehow draw attention to the cluster four nodes in the first graph in the vacuum region that only involve a single variable; this can be done in text or by subtly changing the graphical elements somehow for those four nodes (e.g. changing the font, or the shape of the bubble).

[Terence Tao]

Went through the draft at https://teorth.github.io/equational_theories/paper.pdf . It's getting closer to being done! Besides the Higman-Neumann chapter that @Jose Brox is handling, we basically just need a bit of touchup on Section 7 (proof automation), notably in saying something about semi-automated proof guidance, and whether there are any empirical results we can state (while emphasizing that these are not official benchmarks). Are there any volunteers for some text to provide for these subsections?

This would also be a good time to fill out the contributor section in Appendix B: many of the coauthors are lacking an affiliation. Also, if you have not yet updated contributions.md with your contributions, please do so in a PR (you can see the other PRs marked "contributions" for examples).

[Shreyas Srinivas]

I will add my contributions and affiliation in the next few days.

[Shreyas Srinivas]

Btw, I think my contributions were roughly as follows. Feel free to correct me :

1. I devised the whole project management setup including the schema for the PR management process, essentially a state machine. Pietro implemented this in CI scripts. We had a lot of discussions before the final contributions process emerged.
2. I was doing a lot of firefighting around errors and PRs. I remember helping with some stuck formalisations, though I can't remember which ones.
3. I contributed to the formalisation of one or more anti-implications. (I was actually reminded of something I did from the Big Proof talk slides by Terence Tao that I had forgotten about).
4. I wrote the CI scripts for lean4checker and lean4lean and fixed them with Mario's help. I fixed errors in some parts of the CI every now and then.
5. I participated in the discussions about 1729, but my ideas didn't work out. So I am not claiming that part. I did contribute to its formalisation.
6. I wrote the project management part of the paper

[Terence Tao]

This looks about right to me, but presumably you can search through your old comments in the Equational channel to see if there is anything else that is overlooked. This by the way shows why it is important to get the paper finished while memories are still fresh - it's only been a year and I am also forgetting now what went on (or even what I personally did) inside the project!

[Jose Brox]

Terence Tao ha dicho:

Besides the Higman-Neumann chapter that @Jose Brox is handling,

Another section (or sections) that needs a write-up is, inside Chapter 11, that of the convolutional neural network and transformer results for trying to predict the implication graph, as developed in the thread Machine learning, first results.

This morning I have written a one-page draft for the CNN report, which my colleague Fernando Vaquerizo will complete tomorrow. I have asked @Adam Topaz what he would like to do regarding his transformer results (we could either make separate reports, join them in a single section, or even just skip them, although in my opinion they are valuable).

[Adam Topaz]

Hi! Thanks for the ping. To be honest, I trained that transformer just because I was curious, and unfortunately I didn’t have time to pursue it (or anything else related to the equational project) any further beyond that. So please don’t feel any obligation to mention this in the writeup of the project! Unfortunately I’m still completely swamped at the moment, so that’s unlikely to change.

[Jose Brox]

Jose Brox ha dicho:

This morning I have written a one-page draft for the CNN report

Related to this, in the aforementioned thread I referred to a bit table for the implication graph, weighing 2.75MB, which features in my report. I can't find that file among my folders. At the Github repository I find the outcomes_20241001.png file, which weights 2.33MB; we also have the image at the "Progress visualization" section of the dashboard, but that seems to be compressed, since it weights around 1MB.

Do we have any newer pictures actually weighting 2.75MB? Should I just talk about the 2.33MB picture?

[Jose Brox]

Adam Topaz ha dicho:

I trained that transformer just because I was curious

Isn't that what moves us all? :smile:

Adam Topaz ha dicho:

So please don’t feel any obligation to mention this in the writeup of the project!

If I made a quick summary of your results for the paper, would you mind? In my opinion it doesn't matter that you didn't pursue this further, since this paper is a progress report and yours was a nice work (besides, there are some other unfinished businesses in the paper, like the Higman-Neumann challenge, our own work with the CNN, or even the main project in its finite version).

[David Michael Roberts]

There's a weird stylistic thing in the intro (at least) where sometimes laws are written in an upright font, and sometimes using the standard italic mathematics mode. This is in the text as well as in graphs. Is there any reason for this aside from a final pass not done to unify the notation style?

[Terence Tao]

Fair enough; the numbered equations had been using Roman font and the unnumbered equations italic, but I just went through and changed it to Roman for both.

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

Jose Brox said:

Related to this, in the aforementioned thread I referred to a bit table for the implication graph, weighing 2.75MB, which features in my report. I can't find that file among my folders. At the Github repository I find the outcomes_20241001.png file, which weights 2.33MB; we also have the image at the "Progress visualization" section of the dashboard, but that seems to be compressed, since it weights around 1MB.

---

The dashboard visualization works from two files: a full size png generated during the build, and a lower resolution jpg for previewing/loading. You might be looking at the latter.

I'm traveling in Germany rn, so can't read the dashboard source code right now, but if you open up the source code, the path to this image will be on a line that says something like full: 'path/to/outcomes.png'. This is an always up-to-date file, generated while building the dashboard, so you won't find it in the Github repo.

The file sizes are not really meaningful or indicative at all: pngs are compressed files by default, and as the unknown implications filled in, the compression factor might have changed several times.

[Stanley Burris]

E543 (Tarski's Axiom) on p. 60 of the paper has an extra pair of parentheses ( )

[Terence Tao]

Fixed, thanks!

[David Michael Roberts]

Figure 3's laws are still italic, where figures 1 and 2 has them upright.

Problem 8.1 has a mix of italic and upright for both the laws mentioned there. The law in

ChatGPT was used^16 to guess a complete rewriting system for the law x ⋄ ((y ⋄ y) ⋄ z) ≃ x ⋄ y (E1659)

is, ironically, a mix of italic and upright, which looks to me like an LLM tried to write and/or convert that.

[Bruno Le Floch]

EDIT: I just noticed that the tikz source code is directly in the intro.tex file so anyone can make the change actually. Just to be sure, we want

• the variables to be upright, so \newcommand\x{\mathrm{x}} and use \x etc,
• the equation number in parentheses, with or without (roman-font) E?
• an equal sign, or a \formaleq (with \newcommand{\formaleq}{\simeq}) like in Appendix A?

Maybe $\x \formaleq \x \op \y$ (E4)? That is consistent with the rest of the paper but inconsistent with the Graphiti figures (Figure 1 and Figure 2).

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

The file sizes are not really meaningful or indicative at all: pngs are compressed files by default, and as the unknown implications filled in, the compression factor might have changed several times.

Thanks for your answer! I thought that we had an uncompressed png as original source. Anyway, I have just created a bit table from the outcomes file.

[Jose Brox]

Jose Brox ha dicho:

This morning I have written a one-page draft for the CNN report, which my colleague Fernando Vaquerizo will complete tomorrow.

I already have the LaTeX code for the CNN report (written by me and reviewed by Fernando Vaquerizo), which I think should be included as subsection 11.1 in the paper (also some bibliographic content).

How should I proceed now? Do I just make a PR with the changes in the paper files, or should we produce a task for this first, for me to claim?

[Shreyas Srinivas]

Make the PR directly please

[Shreyas Srinivas]

In this case the task is clearly yours already

[Jose Brox]

I have just made the PR. Please, let us know your thoughts on this new subsection 11.1! It is around 2 pages long

[Jose Brox]

Btw, there seems to be some compilation problem with the to do list.

[Jose Brox]

In a few days will come the Higman-Neumann report, after that my two cents for section 7.

[Shreyas Srinivas]

Do we know how much writing work remains now?

[Terence Tao]

I think @Jose Brox is tackling most of the remaining open sections, perhaps he can give an update? At this point we may simply drop or give very abbreviated versions of any further sections in the paper, and focus on getting to an arXiv-ready state, once the last few contentful sections are in place.

[Shreyas Srinivas]

Sounds good. I could use a nomination in the ITP related topics of arxiv, so when the paper is ready, I'll try uploading it

[Bruno Le Floch]

Remaining tasks AFAICT:

1. Double-check numbers of implications and percentages in the introduction.
2. Reorder the list of methods on page 7-8 or reorder the subsections 5.1–5.6 to match each other. (done)
3. Correct the inconsistent numbers of implications refuted by different magma sizes in section 5.1: it states 13.63M implication were refuted with magmas of size≤4 including 13.34M with size≤3, with the remaining 0.42M requiring size=4, but this does not add up.
4. Currently when referring to Example 2.2 (or Proposition 5.13) we get the word Theorem (so Theorem 2.2, Theorem 5.13), this needs fixing. (done)
5. Section 7.2, paragraph "Proof Reconstruction" concerns how we translate from Vampire proofs (and possibly Prover9, and MagmaEgg) to Lean, I don't know who is in charge of that text.
6. I think the "Semi-Automated Counterexample Guidance" is in Jose Brox' hands.
7. For section 7.3., I think someone (not Jose?) did run some ATPs on each positive implication to see the time they take, so maybe they could report?
8. Section 10 on Higman-Neumann is both Jose's and my fault for being late, I'll see with him whether I take over. (Now Bruno :hammer:.)
9. Section 11 is absolutely opaque to me, does anyone know if the results give better predictions than testing models of sizes 2 and 3? (which seems to have >90% accuracy already)
10. Fix font issue in Appendix A.
11. Complete the affiliations in Appendix B.

[Terence Tao]

I think I dealt with the second bullet point (reording list of methods) and the fourth bullet point (theorem references, it was a cleveref issue).

[Shreyas Srinivas]

Tbh honest I don’t understand that AI section either. What patterns are being learnt and what does the prediction mean? How many pairs of laws had already been resolved before the AI predictions and how did it fare on the rest? What insights have we gleaned from this AI?

[Terence Tao]

Perhaps @Pietro Monticone can weigh in on this. Given that there does not seem to be a very strong variability between models or between metrics, one option is to shorten this section by focusing on one representative model and one representative metric (perhaps selecting the one that is easiest to explain), add some discussion interpreting that result and comparing it (if possible) with some non-ML prediction methods (such as testing against small magma models as Bruno suggests), and mention how things change when working with other models or other metrics but leave the details to a secondary site (e.g., the blueprint). This is broadly in line with other sections of the paper in which we typically focused on a representative sample of a method rather than comprehensively surveying all the use cases of that method.

[Jose Brox]

Bruno Le Floch ha dicho:

• Section 10 on Higman-Neumann is both Jose's and my fault for being late, I'll see with him whether I take over.

I have just sent a quick skeleton of the HN section to Bruno for him to take over. And next week I'm finally free of teaching duties, so I hope I can finish everything that depends on me then.

Bruno Le Floch ha dicho:

• For section 7.3., I think someone (not Jose?) did run some ATPs on each positive implication to see the time they take, so maybe they could report?

I think that's me too, yes :sweat_smile: I timed quite a few different Prover9 and Mace4 configurations for several different implications (I have the results in a file).

[Pietro Monticone]

Terence Tao said:

Perhaps Pietro Monticone can weigh in on this. Given that there does not seem to be a very strong variability between models or between metrics, one option is to shorten this section by focusing on one representative model and one representative metric (perhaps selecting the one that is easiest to explain), add some discussion interpreting that result and comparing it (if possible) with some non-ML prediction methods (such as testing against small magma models as Bruno suggests), and mention how things change when working with other models or other metrics but leave the details to a secondary site (e.g., the blueprint). This is broadly in line with other sections of the paper in which we typically focused on a representative sample of a method rather than comprehensively surveying all the use cases of that method.

Sorry for the delayed response. Things have been extraordinarily hectic on my end these days.

I believe the entire GraphML section should be moved to the supplementary material. The experiments we conducted and reported there months ago are no longer particularly relevant to the main narrative of the paper. They serve more as a test of GraphML methods than as a substantive contribution to the paper itself.

If you agree, I could open a PR removing that section in a few days.

[Shreyas Srinivas]

If that's your preference, personally I agree. I do recommend making a concrete description of the experiments in the blueprint

[Shreyas Srinivas]

To add to the questions, I think we need to establish some sort of a baseline for comparing our predictions and I don't see any obvious candidates here.

[Pietro Monticone]

After re-reading the paper, I honestly don’t think this section is a good fit for either the paper itself or the blueprint. In retrospect, its actual contribution to the project is minimal and does not justify inclusion in the main “narrative”.

[Shreyas Srinivas]

In that case, it’s okay (in my opinion) to make and merge a PR that removes the section I guess.

[Pietro Monticone]

Shreyas Srinivas said:

In that case, it’s okay (in my opinion) to make and merge a PR that removes the section I guess.

Yes, I’ll open a PR in the next few days.

[Shreyas Srinivas]

I can make it now tbh

[Pietro Monticone]

No, I will open it later. Thanks.

[Pietro Monticone]

Done.

[Bruno Le Floch]

• In my list above I forgot "Complete the affiliations in Appendix B".
• In Appendix A, should the letters x,y,... be \x,\y,...?

[Terence Tao]

I fixed the Appendix A font issue. So I guess we can strike off item 9 and add the affilations item to the todo list.

[Stanley Burris]

At the top of page 53 one finds

for instance, the shape of (E4512),
(∗ ⋄ ∗) ⋄ ∗ ≃ ∗ ⋄ (∗ ⋄ ∗), is (∗ ⋄ ∗) ⋄ ∗ ≃ ∗ ⋄ (∗ ⋄ ∗).
Shouldn't the first shape be replaced by E4512?

[Stanley Burris]

In Remark 5.1 on page 22 one finds

It was also shown in [43] that “almost all” finite magmas M (in a certain precise sense) are idemprimal, which implies that their laws are finitely axiomatizable, and all other finite magmas obeying these laws are isomorphic to powers of M.

Perhaps it would be useful to say somewhere that all primals are idemprimal, and all idemprimals are quasiprimal. The
"finitely axiomatizable for idemprimals"
can be strongly improved to
"the laws of any quasiprimal are 1-based, that is, they can be axiomatized by a single equation".
This is a consequence of almost all finite magmas being idemprimal (Murskii), hence almost all finite magmas are quasiprimal, and the fact that all quasiprimals have an equational theory that is axiomatizable by a single equation (Padmanabhan and Quackenbush 1973, on the last page).

Reference:
R. Padmanabhan and R.W. Quackenbush. Equational theories of algebras with distributive congruences. Proc. of AMS, 41(2):373–377, 1973.

The fact that "all other finite magmas obeying these laws are isomorphic to powers of M" applies to all quasiprimals M.

[Stanley Burris]

Some useful facts.
A finite algebra A is:

1) primal if for every n and every function f : A^n --> A there is a term t(x1,...,xn) that expresses f .
This is a well-known property of the 2-element Boolean algebra.

2) idemprimal if for every n and every idempotent function f : A^n --> A there is a term t(x1,...,xn) that expresses f .
f is idempotent means f(a,...,a) = a for all a in A.

3) quasiprimal if the (discriminator) function f : A^3 --> A defined by
f(a,b,c) = c if a =b, and f(a,b,c) = a if a \neq b
is expressed by some (discriminator) term t(x,y,z).
(Clearly such an f is idempotent, so idemprimal implies quasiprimal.)

[Bruno Le Floch]

Regarding associativity (E4512), there are several places (at least p53 as Stanley Burris just mentioned and appendix A) where we write it as (xy)z=x(yz), whereas with our conventions it should be x(yz)=(xy)z instead.

[Terence Tao]

I've updated the paper with these comments.

[Stanley Burris]

The convention of using different fonts for M, depending on whether one is referring to a magma or its carrier, has not been always adhered to. See for example page 24. This convention should also apply to groups G, rings R, etc? What about M_X as a magma and its carrier?

---

The paper by Tarski on page 58 is stated as Ein beitrag zur axiomatik der abelschen gruppen.

Proper German would read :
Ein Beitrag zur Axiomatik der abelschen Gruppen.

[Terence Tao]

Fixed, thanks.

[Stanley Burris]

Regarding the use of symbols for equality. This topic can lead to subtle and involved discussions that belong in a logic course.
But perhaps a remark on the use of the symbol "≃" in this paper is appropriate, namely about when to use this symbol and when to use "=".

On page 23, Example 5.2, one has

For the law x = y ⋄(((x⋄y)⋄x)⋄y) (E1286),

and on page 24, Example 5.7, one finds

For the law x ≃ (x ⋄ y) ⋄ ((x ⋄ y) ⋄ y) (E1648),

On page 26 both symbols of equality are used:

Example 5.11. We compute the twisting semigroup of
x ≃ (y ⋄ x) ⋄ (x ⋄ (z ⋄ y)) (E1485).
We test this law on the operation Equation (8), thus we consider whether
x = (y ⋄′ x) ⋄′ (x ⋄′ (z ⋄′ y))
holds for all x, y, z ∈ M.

[Cody Roux]

The last one seems appropriate imho: we're talking about equalities which hold "on the nose" in M.

[Douglas McNeil]

Are we aiming to submit in 2025? Seems achievable at this point, after rather a long tail when everyone was off earning a living!

[Shreyas Srinivas]

I hope we do. There is not much left and we'd all like to say "we did this"

[Jose Brox]

Pietro Monticone ha dicho:

No, I will open it later. Thanks.

Pietro, you erased the entire section 11, but we have yet our ANN experiment pending of merge for that section, so we could still use the introduction we had for the section. Can you restore it, or it is better if I just re-include it with my merge?

[Shreyas Srinivas]

You can get the content from the diff of the closed PR

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/blob/b93f4b206e0d10e44b01c863189d2a0795361366/paper/conclusions.tex

[Shreyas Srinivas]

Sorry I think the ML file is missing there. Here's the ml.tex file before the PR removing it was merged:
https://github.com/teorth/equational_theories/blob/f6347349100bc9d730a5b755ce7d4770ab6a1d16/paper/ml.tex

[Pietro Monticone]

Oh sorry @Jose Brox. Didn’t know about that. Feel free to re-include it with your merge removing only the directed link prediction section. Thanks.

[Stanley Burris]

Correction to Footnote 9, page 22 [This was my error!]

quasiprimality is sufficient to show that all other finite magmas obeying the laws of $M$ are isomorphic to
powers of $M$

This should read:
"are isomorphic to products $M_1^{n_1} \times \cdots\times M_k^{n_k}$ of powers of the submagmas $M_1,...,M_k$ of $M$"

[Stanley Burris]

For a historical note, quasiprimal algebras played a key role in the difficult question of determining which varieties V generated by finitely many finite algebras have a decidable first-order theory. (The equational theory of V is obviously decidable, since an equation E holds on all members of V iff it holds on the finitely many finite generators.)

There are simple tests to determine if a quasiprimal A is idemprimal or primal, namely
1) A is idemprimal iff it is rigid (the only automorphism is the identity map on A) and any subalgebra of A that is not A is trivial (only one element);
2) A is primal iff it is idemprimal and its only subalgebra is A.

The only 2-element quasiprimal magma is the Boolean algebra (with the Sheffer stroke), and it is primal.

However one can distinguish quasiprimal from idemprimal from primal with 3-element magmas. (This was pointed out to me by Marcel Jackson of La Trobe University in Australia.)

[Stanley Burris]

I am a little concerned about the convention on page 3 for the use of the symbol $\vdash$ as it is contrary to what Sanka and I adopted for our book of 1981. So I took the risky step of asking ChatGPT about the meaning of "entailment" and was amazed to see that I completely agreed with it. As food for thought I pass the chat on to you:

Chat with ChatGPT

What symbol is used to express one equation entails another equation?

In logic and mathematics, the symbol used to express that one equation entails another depends on the context—syntactic or semantic. Here’s the breakdown:

---

1. Semantic entailment (meaning-based):

Symbol: $\models$
Usage:

$E_1 \models E_2$ means that in every interpretation (or structure) in which the equation $E_1$ holds, the equation
$E_2$ also holds.

Read as:
* “$E_1$ semantically entails $E_2$”

• or “$E_2$ is a semantic consequence of $E_1$”

• or “whenever $E_1$ is true, $E_2$ is true.”

Example:

$x = y \models x + z = y + z$

In every algebraic structure where $x = y$ is true, so is $x + z = y + z$.

2. Syntactic entailment (provability in a deductive system):

Symbol: $\vdash$
Usage:
$E_1 \vdash E_2$
means that $E_2$ can be derived from $E_1$ using a system of inference rules.
Read as:
* “$E_1$ proves $E_2$”

• “$E_2$ is derivable from $E_1$”

• “$E_2$ follows from $E_1$ by formal proof.”

[Table for 3. Summary of Usage not copied here.]

If you’re working in universal algebra or equational logic, the semantic entailment $\models$ is usually the appropriate symbol to express that one equation entails another (i.e. holds in all algebras where the first holds).

[Terence Tao]

Fair enough, I've changed the entailment symbol and the footnote.

[Stanley Burris]

Perhaps an example from ring theory will put the two notions of entailment, namely $\vdash$ and $\models$, in sharper relief.

Using $\vdash$ vs using $\models$

Let RngAx be a collection of axioms for rings.
In Herstein's book Topics in Algebra one finds the following three exercises over a few dozen pages:

RngAx with $x^2=x$ implies $xy=yx$
RngAx with $x^3=x$ implies $xy=yx$
RngAx with $x^4=x$ implies $xy=yx$

Students are expected to solve each of these by the simple means of manipulating equations, like obtaining $(x+y)^2 = x+y$ in the first case, and then expanding the left hand size, etc. The first exercise is rather easy, the second is more demanding, and Herstein told me that he had more correspondence on the third than any other exercise in his book. And many a mathematician has played with higher values of $n$, trying to prove by such elementary means that

RngAx with $x^n=x$ implies $xy=yx$.

Here the value of $n$ is fixed for each proof. A proof by such means would be an example of showing that

RngAx , $x^n=x \vdash xy=yx$.

One has a precisely described deduction system, say Birkhoff's equational logic, with precisely described options for generating new equations. No appeal is made to look at the structure of rings. It has the flavor of combinatorics.

In 1945 Jacobson gave a single proof that for all $n \ge 2$ one has
RngAx with $x^n=x$ implies $xy=yx$
by examining the impact on a ring R of requiring that it satisfy
$x^n=x$. One is really bringing set theory into play looking at ideals and homomorphisms with the option to bring in any set constructions that seem useful. For this kind of proof we write

RngAx , $x^n=x \models xy=yx$.

It is common to view the world of proofs found by computers as belonging to the syntactic side ($\vdash$), whereas invoking models, often infinite, belongs to the semantic side ($\models$) on the grounds that a computer cannot verify an assertion by trying infinitely many or infinitely large models.

These distinctions, syntactic vs semantic, begin to blur as ATP systems become capable of inventing and using set-theoretic constructions and reasoning in the quest for a proof. But now I am getting into philosophical questions about the future of mathematics, so time to stop.

[Stanley Burris]

Data and examples on 3-element magmas.

In collaboration with Marcel Jackson we have the following:

1) The number of primals is 629.

2) The number of idemprimals that are not primal is 777.

3) The number of quasiprimals that are not idemprimal is 79.

100 020 000 is primal.

001 020 102 is idemprimal, not primal.

001 021 211 is quasiprimal, not idemprimal.

This information was independently extracted by both of us from the B&B catalog of 3-element magmas by hand following Marcel's discovery that one could separate the notions of primal, idemprimal and quasiprimal by such magmas.

[Kevin Buzzard]

The claim that for all n>= 2, (for all x, x^n=x => R is commutative) must have some content, because it implies the delicate (but standard) result that a finite division ring is a field (and hence that the Brauer group of a finite field is trivial). Apparently Jacobson proved an even stronger result: if for all x in a ring, there exists some natural n(x)>=2 such that x^(n(x))=x, then R is commutative.

[Terence Tao]

I now remember thinking some months ago when writing portions of the paper that due to the Birkhoff completeness theorem, this particular distinction wasn't an issue for magmas and one could use $\vdash$ and $\models$ interchangeably. But we also consider the analogue $\models_{\mathrm{fin}}$ of semantic entailment for finite magmas, and in this case we don't have a complete syntactic calculus (or at least, we have not proposed one - we have some additional axioms like surjunctivity, but it is unlikely that they are complete), so the distinction is certainly relevant here.

[Shreyas Srinivas]

we prove almost all positive implications syntactically right?

[Stanley Burris]

@Kevin Buzzard Thanks for pointing out that one certainly needs
$n\ge2$, and that the result "for all $n\ge2$" is certainly much stronger than the particular cases $n=2$, etc. I know some mathematicians have tried to give an algorithm which for each $n\ge2$ shows how to write down an elementary (equational logic) proof that $xy=yx$, where we are justified in using $\vdash$, but I do not know if such an algorithm has appeared anywhere.

A set theorist could point out that Jacobson's strong result proving that $x^{n(x)} = x$ implies commutativity can be written up as a single (formal) sentence $\varphi$ in the language of ZFC, and thus one would write ZFC $\vdash \varphi$, or simply $\vdash \varphi$ if the context is one of working with formal proofs in ZFC. The distinction between $\vdash$ and $\models$ evidently depends on whether or not one is looking at a proof in the context of a formal system (like ZFC, or Birkhoff's equational logic), or in the context of an informal system (like naive set theory). And probably one would write ZFC $\models \varphi$ if one is claiming that every model of ZFC satisfies $\varphi$ in the context of naive set theory. The context of a formal mathematical system would evidently be the metamathematics for that system.

In 1968, when the Hungarian logician Kalmar was visiting UWaterloo, he said (as best I can remember) that one could have a hierarchy of contexts, each one being a metasystem for the previous level. This is all great material for the philosophy of mathematics, but a rather rich diet for my tastes. (Kalmar, by the way, was the young mathematician who fixed a problem with Landau's course notes on the foundations of mathematics where Landau was falsely claiming to use the axiom of choice to define the usual operations on the natural numbers. This inspired Landau to publish his famous Grundlagen der Analysis.)

By the way, Herstein comments towards the end of his book that the strongest form of Jacobson's result requires the Axiom of Choice, a digression that he declines to take in his book. I do not know the status of that claim today.

[Terence Tao]

Shreyas Srinivas said:

we prove almost all positive implications syntactically right?

Technically the lean formalization uses the semantic interpretation, but for infinite magmas it was checked that Vampire could establish all positive implications via syntactic rewriting. For some finite magmas implications we used ad hoc semantic arguments eg there is one based on the cycle decomposition of permutations.

[Alex Meiburg]

Well, Birkhoff doesn't apply for the finite magmas, right? So that will be necessary. (I want to write "that will be necessarily necessary for some" ... but I won't. :slight_smile: )

[Cody Roux]

I'm a little confused so I'll just write down what I think I understand and people can correct me:

1. Birkhoff's theorem does hold for equational logic: if an equation is entailed by others, then there is a syntactic proof. And indeed, if we know that the entailment holds (and the set of assumed equations is finite), there is an algorithm to find it: just enumerate all the proofs. It is cool that Vampire does actually find them though.
2. It sounds like the theorem @Kevin Buzzard alluded to is: fix a natural number $n \geq 2$. Then, if $R$ is the first order theory of rings, then $R\cup \forall x, x^n = x\models \forall x y, x y = y x$. If that is the case, then the completeness theorem for first order logic applies, and we can replace $\models$ with $\vdash$. I certainly know how to do the proof for $n=2$, but maybe it gets harder for larger $n$. Again, one can find some trivial algorithm to do this, by just enumerating proofs.
3. The statement $\forall x\exists n\geq 2, x^n = x$ is not a statement in the first order theory of rings, so the same does not apply.

[Jose Brox]

Terence Tao ha dicho:

due to the Birkhoff completeness theorem, this particular distinction wasn't an issue for magmas and one could use $\vdash$ and $\models$ interchangeably.

Yup, and this is true more in general in the setting of (first-order) model theory thanks to Gödel's _completeness_ theorem (symbolic provability amounts to semantic truth). This is relevant to us, since we don't restrict to universal algebra -we often add other first-order conditions like injectivity of some map, and we are always negating some sentence.

Terence Tao ha dicho:

But we also consider the analogue $\models_{\mathrm{fin}}$ of semantic entailment for finite magmas, and in this case we don't have a complete syntactic calculus (or at least, we have not proposed one

We cannot give a syntactic calculus for the finite setting, at least not within first-order logic: by the upward Löwenheim-Skolem theorem (a straightforward corollary of the compactness theorem), if a first-order theory has arbitrarily large finite models, then it has infinite models.

For a while I tried to find some higher-order characterization of finite cardinality that we could effectively use in Vampire (which is able of managing higher-order), but I didn't succeed, in part because the HO logic in Vampire doesn't seem to be well documented anywhere. I think this tool, if at hand, would be quite useful, particularly for 677 anti 255.

[Stanley Burris]

As regards the three items of @Cody Roux:

1. ...there is an algorithm to find it: just enumerate all the proofs.

Indeed that fits the meaning of algorithm, but those trying to find an algorithm were looking for a direct method with "no unnecessary steps", all steps focused on how to write down the formal proof. It seems they also wanted one where the computational complexity is not too great so one can find the proof by hand for small $n$.

2. ...but maybe it gets harder for larger $n$.

Indeed it gets harder for $n$ increasing from 2 to 4.

3. ...is not a statement in the first order theory of rings, so the same does not apply.

Agreed! One could translate an informal proof of such a statement into a formal proof in first-order logic, in ZFC, so perhaps Jacobson's theorem can be proved by an ATP someday.

[Stanley Burris]

Here is an M font issue on page 10.

or of the form $w_1 ⋄ w_2$ with $w_1,w_2 ∈ MX$.

Perhaps one could be more precise by saying "a string of symbols
$w_1 ⋄ w_2$ from $X\cup\{\diamond,(,)\}$".
Using infix notation leads to a need for parentheses as in $(w_1 ⋄ w_2)$, with the readability convention that one drops outer parentheses, or one could use $(w_1) ⋄ (w_2)$ without the need to drop outer parentheses. But then one would not want to use parentheses on single letters.

And perhaps some more M font issues on this page

a map ιX,Γ : X →MX,Γ
of a word w ∈ MX

There are more M font issues on page 36

On page 21 one finds

refuted with 3 × 3 magmas, with the remaining 415, 293 requiring 4 × 4
magmas.

One would not say that a 3-element group is a 3 x 3 group, but the table would be 3 x 3.

On page 38 one has

$x_i = (((w^′_1 ⋄ w^′_2) ⋄ v_1) ⋄ . . . ⋄ v_i).$

Should this be

$x_i = (\cdots((w^′_1 ⋄ w^′_2) ⋄ v_1) ⋄ \cdots)⋄ v_i.$

using the "drop the outer parentheses convention, and noting that there could be lots of parentheses on the left end?

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

@Jose Brox: Trakhtenbrot's theorem prevents the existence of any complete syntactic calculus for implications in finite structures.

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

I don't even know a higher-order condition which holds in all finite structures and suffices to show something like the Artin-Zorn theorem (although presumably one could extract one from the proof), so I'm not hopeful for conditions that could really help with 677.

[Bruno Le Floch]

Regarding 677, I think a more promising approach is to build the model a bit like Terry Tao built his 232-element megamagma (countermodel to 1518⊨47), but with a much more complicated linear fall-back instead of the projection operation he used for 1518. But first let's finish the paper. Higman-Neumann section incoming this afternoon.

[Stanley Burris]

Short of writing detailed notes on an introduction to universal algebra it seems that I am near the end of my editorial comments, trying to keep in mind two famous quotes:

1. Ralph Waldo Emerson, “A foolish consistency is the hobgoblin of little minds, adored by little statesmen and philosophers and divines.”
2. Bertrand Russell, “A book can be either correct or interesting, but not both.”

Some more M-font items:
page 10: every function f : X → M
page 24: numerous M-fonts, starting with: the carrier M is now an abelian group,
page 24: take M to be the group
page 30: six G-fonts
page 31: two M-fonts (including End(M) ?)
page 45: when the magma M is finite,
page 51: A key feature of finite magmas M

In other directions:

page 41: "equational reasoning is a type of reasoning based on equational logic and rewriting with congruence [6]."

For universal algebraists equational reasoning is based on Birkhoff's 5 rules of inference: Reflexive, Symmetric, Transitive, Replacement and Substitution.

page 41: 'takes a series of equations and determines whether".
For ATPs, replace "determines" by "tries to determine". There is no decision procedure.

page 46: "how many finite magmas exist of each size in the spectrum."

The number of finite magmas of each size is called the fine spectrum in
W. Taylor — “The fine spectrum of a variety.” Algebra Universalis 5 (1975), 263–303.

and there are the closely related

Joel Berman & Paweł M. Idziak — Generative Complexity in Algebra. Memoirs of the AMS, 2005.
— Thorough monograph on the generative spectrum (how many non-isomorphic algebras are generated by $k$ elements) for locally finite varieties.

Kamilla Kátai-Urbán, András Pongrácz & Csaba Szabó — “The fine- and generative spectra of varieties of monounary algebras.” Algebra Universalis (2019).

M. Bilski — “Generative complexity in semigroup varieties.” Journal of Algebra (2001).
— Studies generative complexity in semigroup varieties; cites Taylor on fine spectrum and explores related enumeration problems.

page 51: What is meant by a "definable map from M to itself" ?

[Alex Meiburg]

Stanley Burris said:

page 51: What is meant by a "definable map from M to itself" ?

It explains at the end of that sentence:

where “definable” is with respect to the language of magmas.

as in, https://en.wikipedia.org/wiki/Definable_set

[Terence Tao]

Some more M-font items:
page 10: every function f : X → M
page 24: numerous M-fonts, starting with: the carrier M is now an abelian group,
page 24: take M to be the group
page 30: six G-fonts
page 31: two M-fonts (including End(M) ?)
page 45: when the magma M is finite,
page 51: A key feature of finite magmas M

Actually most of these (except the last two) are intentional! I am trying to consistently use the italic M rather than the calligraphic M when the magma structure on M is not being used (but other structures such as group or ring structure are permitted). In particular functions on M that are not magma homomorphisms (as opposed to group homomorphisms, where the group operation is distinct from the magma operation) should not use the calligraphic M.

I've implemented the other suggestions, thanks!

[Bruno Le Floch]

Higman-Neumann section done, see PR https://github.com/teorth/equational_theories/pull/1325

• In section 4, there is a mention of an @[equational] attribute, should it be @[equational_result] (with some extra formatting, see other occurrences in the file)?
• Section 4 mentions an "aforementioned free magma issue" but I didn't see it, has it been removed from the text perhaps?
• Section 5 still has inconsistent numbers of implications treated by each magma sizes, my code checking these numbers should finish running overnight and I will report here.
• In Section 6 (metatheorem.tex), I think the following should use $M_X$ since a canonizer is not a magma morphism: « In fact, a canonizer is simply a matching invariant with target in $\Magma_X$. ».
• Also in that section. The layout and font of definitions makes it very unclear where Definition 6.7 ends, so it is hard to understand the hypothesis of Theorem 6.8 « Whenever R satisfies all the conditions of Definition 6.7 ». Maybe we should list the conditions explicitly (weakly collapsing, weak canonizer, non-overlapping). Another unpleasantness is that we want equations lhs≃rhs in which rhs is simpler than lhs, but in our conventions everywhere else, lhs is simpler instead.

[Shreyas Srinivas]

Bruno Le Floch said:

Higman-Neumann section done, see PR https://github.com/teorth/equational_theories/pull/1325

• In section 4, there is a mention of an @[equational] attribute, should it be @[equational_result] (with some extra formatting, see other occurrences in the file)?

Feel free to change this and fix it in your PR. It is too small an issue to require a new PR.

• Section 4 mentions an "aforementioned free magma issue" but I didn't see it, has it been removed from the text perhaps?
  

I think it was mentioned in the text at some point. Basically we built a whole theory of free magmas while mathlib had one.

[Jose Brox]

Pietro Monticone ha dicho:

Feel free to re-include it with your merge removing only the directed link prediction section.

I just did this, expanding a little bit the footnote about other approaches, just to mention they are a GNN and a transformer (with their respective links to Zulip), and I resolved the nice comments by @Douglas McNeil. The section is ready to merge again.

[Terence Tao]

I implemented Jose Bruno's suggestions (except for not messing with the lhs/rhs issue for canonizers, as I see no easy way to flip the notation without potentially causing other problems). Getting very close to the finish line! I will start DM'ing people who haven't yet filled in their affiliation and/or contributions to do so.

[Stanley Burris]

Some definitions:
The order of a magma does not seem to be defined in the paper. It first appears on page 8

order equal to a perfect square $n^2$;

The order of a finite magma is implicitly defined on page 21:

A finite magma ${\mathcal M}$ of order $n$ can be labeled by the carrier $\{1, . . . , n\}$

The phrase "can be labeled by" is more precisely captured by "can be assumed to have" and then add "by replacing ${\mathcal M}$ by an isomorphic copy if necessary".

I usually prefer the carrier $\{1, . . . , n\}$ to $\{0, . . . , n-1\}$, but there are set-theoretic reasons for choosing the latter. Namely for $J$ a non-empty set one usually defines ${\mathcal M}^J$ to be the magma with carrier $M^J$, being the set of functions from $J$ to $M$. Then for $f,g \in M^J$ one has $f=g$ iff for all $j\in J$, $f(j) = g(j)$, and $f\diamond g$ is defined by $(f\diamond g)(j) := f(j) \diamond g(j)$. But then to carry this over to ${\mathcal M}^n$ for $n$ a positive integer set-theorists use the fact that in set-theory one has $n = \{0,\ldots,n-1\}$.

[Jose Brox]

Stanley Burris ha dicho:

The order of a magma does not seem to be defined in the paper.

(As I've done all along the project) I propose we use size instead of order, already in use in some sections like Higman-Neumann, spectrum, counterexample constructions...

[Terence Tao]

This makes sense, especially as we are already using "order" in a different sense, namely the order of an equational law. Will implement the change now.

[Terence Tao]

As we are getting very close to the finish line, I think we can triage the potential discussion about evaluating the performance of different ATP tools, as we never really got the chance to do any meaningful controlled experiments in this area. I suppose this is always something that a future project can experiment with though.

Other than that I think we are pretty much done - one or two more affiliations, and finish doublechecking the various statistics reported, and we might be good to submit to arXiv soon!

Regarding journals, we currently have a tie in the Aug 6 poll above between Annals of Formalized Math and Journal of Automated Reasoning, but not all co-authors have voted. Perhaps there are some other co-authors who want to weigh in? Otherwise it may just be a coin flip.

[Bruno Le Floch]

I think @Jose Brox has worked on section 7.3 in the past few days (re-running some experiments with various parameters), maybe he can chime in with whether he can be done with it quickly or not.

Link to poll: #Equational > Writing the paper @ 💬 It was announced as not-a-referrendum, and I also see a deleted account has voted, maybe everyone has to check they're happy with their vote.

[Terence Tao]

Bruno Le Floch said:

I think Jose Brox has worked on section 7.3 in the past few days (re-running some experiments with various parameters), maybe he can chime in with whether he can be done with it quickly or not.

Link to poll: #Equational > Writing the paper @ 💬 It was announced as not-a-referrendum, and I also see a deleted account has voted, maybe everyone has to check they're happy with their vote.

Ah, didn't realize that. If Jose (or anyone else) is willing to volunteer to report on these statistics (I have currently commented out these sections for lack of content), that would be great!

We could redo the poll if needed; happy to do that if there is interest in doing so.

[Jose Brox]

Terence Tao ha dicho:

Ah, didn't realize that. If Jose (or anyone else) is willing to volunteer to report on these statistics (I have currently commented out these sections for lack of content), that would be great!

Yes, I confirm I'm working on it! :smile: I was redoing some experiments, and trying to synthesize what I can really say. About comparing ATPs properly I only have two small (but informative) comparisons between Vampire and Prover9, I have more info about tweaking Prover9/Mace4, comparisons between sets of parameters with specific examples. Also some basic comments on semiguidance and such, how times are improved adding other constraints, and how we integrated the ATPs with SAGE. In addition, during the project I experimented with other interesting Prover9 features like semantic guidance and addition of hints, but they didn't work for me and I don't think it is useful to say so (perhaps it was just me not doing things well enough). On the other hand, I would like to mention the isofilter bug we found, and some other basic comments regarding the GUI versus the terminal (see below), which can be useful for unaware new users (but I'm a bit hesitant about their real value for our paper, perhaps you can give your opinion about this).

I have also run into some problems (for example for logistic reasons I had to use 3 different combinations of hardware/software, that I need to compare now), the biggest one being the following: the GUI uses a previous version of Prover9/Mace4 (the latest one can only be used via terminal), but in my experience it seemed to be sometimes faster than the latest one! This I have confirmed these days with a dramatic example: the longest Prover9 proof, found in the HN subproject (which originally needed several computation hours to be found), can be found in 8 minutes with the GUI with max_weight 300 and sos_limit 200. In startling contrast, with the same parameters, the latest version fails to find a proof, exhausting the search after several hours (9h in a slightly slower machine). Idk if this is due to some default parameters not being actually the same in the two versions (shouldn't be the case if I have read the manual and the GUI options correctly, which I've done carefully these days), or to an important behaviour change in the latest version with respect to the GUI one; in any case, that the behaviour is quite different is evidenced by the clauses statistics found in the output files, which differ significantly between both versions.

I'd really like to be able to warn about this problem by identifying its cause (a priori, from the statistics differences one should be able to infer where the problem lies), but I fear it would imply learning the inner workings of some very specific inference processes of Prover9 (I tried to reach McCune before realizing that he sadly died in 2011... Also asked @Zoltan A. Kocsis (Z.A.K.) in case he knows how to identify the problem, but I think he hasn't read me yet).

All in all, I think that in the end I will be happy adding several small paragraphs to the paper, so not much information, but (hopefully) interesting nonetheless.

[Stanley Burris]

Out of curiosity I just read some information on the new overlay journal Annals of Formalized Math and was surprised by how different it was from the Journal of Automated Reasoning. Perhaps it would help the co-authors make a choice if they saw a comparison of the features of the two journals, like who holds the copyright, is it open access, etc.

[Kevin Buzzard]

I would ask someone like @Michael Kinyon about Prover9 questions, perhaps if he can't answer then he'll know who to talk to.

Annals of Formalized Math is diamond open access so (at least as far as I am concerned) it is maximally optimal when it comes to treating its authors correctly. If you have questions about it then there are people on this Zulip such as @Filippo A. E. Nuccio who I'm sure would be happy to answer them.

[Shreyas Srinivas]

Kevin Buzzard said:

I would ask someone like Michael Kinyon about Prover9 questions, perhaps if he can't answer then he'll know who to talk to.

Annals of Formalized Math is diamond open access so (at least as far as I am concerned) it is maximally optimal when it comes to treating its authors correctly. If you have questions about it then there are people on this Zulip such as Filippo A. E. Nuccio who I'm sure would be happy to answer them.

My only counterpoint is that publication at an established venue is more beneficial to young researchers

[Jose Brox]

Shreyas Srinivas ha dicho:

My only counterpoint is that publication at an established venue is more beneficial to young researchers

As a junior postdoc in Math, with my career still much affected by journal statistics, I've anyway casted my vote for Annals of Formalized Math, because the Journal of Automated Reasoning is only listed in the "computer science, artificial intelligence" category of the JCR, and there only in position 186/204 (Q4) with a JIF of 0.8 and a JCI of 0.21.

On the other hand, the Annals of FM has diamond access and, by reading the description, aims and scope, is completely suited to our paper (mathematical audience, formalization and ATPs as main tools, description of the mathematical lessons learned while using the tools...).

[Jose Brox]

Regarding Annals of Formalized Mathematics, will we be able to satisfy this condition?

"Authors are required to provide a permanent Software Heritage persistent ID (SWHID) of the repository containing their code. As Software Heritage regularly crawls open code repositories, chances are that their code already has a SWHID, that can be checked here: if not, they can request one"

[Shreyas Srinivas]

One small thing: could we avoid using capital case for the author list?

[Terence Tao]

I think this is a default of the amsart document class, but am happy to switch to any other standard document class. (But some of the journals we are discussing may have a house style already; I haven't checked.)

[Shreyas Srinivas]

Ah okay. I think some CS templates like acmart also have all caps author names but they also usually list one author per line.

[Jose Brox]

A related small comment: we should homogeneize the (sub)sections case style, right now we have some in sentence case (e.g. "Further directions") and others in title case (e.g. "Magmas and Equational Laws"). I suggest we always use sentence case (only first word capitalised).

[Bruno Le Floch]

On the topic of subsections, probably subsections 10.1, 10.2, 10.3 should be downgraded (to paragraph? textbf?) as they give too much importance to that particular side-quest. Subsections 11.1 and 14.1 are alone in their sections so they also look odd.

[Jose Brox]

Also very minor: When we say "The specific mathematical goal was inspired by a MathOverflow question", shouldn't we specify the question and/or provide a link?

[Terence Tao]

OK, I think I have implemented these changes.

[Stanley Burris]

more minor changes to consider:

page 3: "assignments of the indeterminate" appears twice.
Change indeterminate to indeterminates.

page 5: Section 1.3. "and non-implications $E \not{\models} E′$ magmas formalized in"
Delete the word magmas?

page 7: for Figure 3. "above/below law 3 can"
Change law 3 to law (E3)

page 7: in Linear models: "automatically scanned for either"
Insert comma: automatically scanned for, either

page 9: in section 1.4: "namely magmas satisfying them"
Change to "namely with magmas satisfying them"

[Jose Brox]

Terence Tao ha dicho:

OK, I think I have implemented these changes.

I think something didn't go well: 11.1 is still there, the subsections of 10 lost their numberings, 7.1 lost its number but now 7.2 is 7.1, and all subsections without numbering (including former 14.1) are still seen in the TOC and at the highest level.

[Terence Tao]

Ugh, that does look pretty bad. I've reinstated the subsection numbers but now set the table of contents depth to 1, let's see if that looks any better.

[David Michael Roberts]

@Shreyas Srinivas I think "coauthoring a paper with Terry Tao and a bunch of other interesting mathematicians" (sorry Terry) trumps "but this journal is tOo YoUnG!"

[Jose Brox]

Jose Brox ha dicho:

Regarding Annals of Formalized Mathematics, will we be able to satisfy this condition?

"Authors are required to provide a permanent Software Heritage persistent ID (SWHID) of the repository containing their code. As Software Heritage regularly crawls open code repositories, chances are that their code already has a SWHID, that can be checked here: if not, they can request one"

@Shreyas Srinivas What is your take on this?

[Shreyas Srinivas]

I gather we can always create a zenodo archive from a specific tag/commit and create a SWHID for that.

[Shreyas Srinivas]

But this is a question to be addressed to one of the journal editors.

[Shreyas Srinivas]

In venues which care about verifying and preserving software artefacts (thinking of CS conferences here), there is usually a well-established system for producing artefacts that the venue finds acceptable

[Shreyas Srinivas]

Interestingly, they haven't automatically archived equational theories yet. https://archive.softwareheritage.org/browse/search/?q=github.com%2Fteorth%2F&with_visit=true&with_content=true

[Douglas McNeil]

Has two forks from last year, though; guess they don't automatically chase upstream.

[Shreyas Srinivas]

Personally I prefer uploading to Zenodo and making an link out of that

[Shreyas Srinivas]

Firstly, it is an EU service. Secondly, it is the defacto standard in many areas of CS

[Shreyas Srinivas]

and thirdly, we want to keep track of the version we submitted the article with.

[Shreyas Srinivas]

But this is ultimately the journal editors' decision

[Pace Nielsen]

page 3: The paragraph starting with "We also define a variant..." has four sentences. The first two sentences are the same as the last two, so those last two should be deleted. Also, the symbol M is never used, and should probably be deleted from the first sentence.

page 9: Near the bottom is a \phi which should be a \varphi (when defining the free magma on X and \Gamma).

If we want to have the author names (and/or the title) use normal upper/lower casing on the first page, there is an easy way to do that while keeping the amsart style. Replace the \maketitle line with the following:

\begingroup
\def\uppercasenonmath#1{} % this disables uppercasing title
\let\MakeUppercase\relax % this disables uppercasing authors
\maketitle
\endgroup

The paper looks great so far!

[Stanley Burris]

page 19: change "These tools checks something" to "These tools check something"

page 57: change "is a doctoral students at" to "is a doctoral student at"

A style consideration: When to write E43 vs (E43)
My preference would be to use the parentheses only when

1. cataloging the laws as on pages 58--60
2. used as additional info, as in "the law x ⋄ y ≃ y ⋄ x (E43)", an alternative to writing "the law x ⋄ y ≃ y ⋄ x, E43,"

[Pace Nielsen]

Page 21, last line (preceding Remark 5.1). "had an size" -> "had a size"

Page 23, last paragraph (preceding Subsection 5.3). In the phrase "commutative and noncommutative models" add the word "linear" before "models".

Page 24, line 4. Change M= (M,+) by replacing the first M with a script M. A similar change to M=(M,\cdot) should occur three lines later.

Page 25, paragraph after Remark 5.10. "by translation-invariant models" -> "to translation-invariant models".

Page 26, near the bottom. Change "this particular implication ...easily established..." by either replacing "implication" -> "non-implication" or replacing "established" -> "refuted" (but not both).

Page 31, 5.6(ii). In the phrase "in such a way that $N$ satisfies" the $N$ should be a script N.

Page 33. In the phrase "that violated E eventually succeeded", should E be replaced by E413?

Page 36. There were a lot of issues on this page starting with Definition 6.7 and proceeding through 6.8.

First, it was unclear to me why there is a "(weakly)" in the first bullet point. Just call it "collapsing" unless there is a good reason to call it "weakly collapsing", in which case the parentheses should be removed and the word "weakly" should be italicized. It might make sense to change "sub-word" -> "(not-necessarily proper) sub-word" in any case.

Second, in the second bullet point, the notation \theta(w)=w\theta is introduced. In my experience, it is a very bad idea to introduce notation that rearranges the order of symbols. This is often a sign of trying to hide important information in the notation, and often leads to very ugly (and hard to follow) equations. Thus, I recommend using \theta(w)=\theta w.

In other words, dropping the parentheses is fine. Reversing the order is not.

Third, in the third bullet point, again is there a reason for the qualifier "weak"? If not, it should be dropped.

Fourth, the numbered equations (10)-(14) should not be numbered.

Fifth, isn't the (currently) numbered equation (12) true simply from the definition of C_R?

In fact, after some work I still cannot follow this string of equalities. Here is as far as I got. Start by writing $l=a\diamond b$. This holds since $l$ is not a variable, as part of the hypothesis that $R$ is a canonizer. We then have

$$C_R(\theta l) = C_R(\theta a \diamond \theta b)=R ((C_R\theta) a\diamond (C_R\theta) b)$$

Now, we want to apply the fact that R is a canonizer. To do that we need to know that $(C_R\theta)a \diamond (C_R\theta)b$ is some substitution applied to $l$. Note that $a$ and $b$ are proper sub-words of $l$, so if they are not variables then the fact that $R$ is non-overlapping comes into play. But if they are variables, then something else occurs.

As best as I can guess, we are now doing another induction, to claim that $C_R\circ \theta$ is a substitution on proper subwords of $\ell$. Anyway, even after that, does this mean that $C_R\circ \theta$ is a substitution on $r$? Thus, the last two equalities are very hard for me to see.

Maybe $C_R\circ \theta$ is being viewed not as the composition of two functions, but rather as the substitution generated by the map $C_R\circ \theta$ acting on variables? If that's the case, a better notation might be $\theta^{\ast}$ for the substitution generated by $\theta$. Then the equality looks something like

$$C_R(\theta^{\ast} l) = C_R(\theta^{\ast} a \diamond \theta^{\ast} b)=R ((C_R\theta^{\ast} a)\diamond (C_R\theta^{\ast}b))=R((C_R\circ \theta)^{\ast}l)=...$$

[Cody Roux]

I wrote this bit, I'll respond in detail later but certainly we can change things to make them clearer.

[Cody Roux]

I will note though that the qualifiers and notation funkiness is because of standard notations and definitions in rewrite theory: substitutions are applied postfix and collapsing has a standard (different but related) meaning.

[Pace Nielsen]

Cody, thanks for the clarification. (And apologies if my wording came across aggressively!) Using "weakly collapsing" (with no parentheses) seems like a good choice.

There is another place where symbol reversal is very common--- the conjugation notation $a^g =gag^{-1}.$ This leads to some very "funky" looking equations that could be completely avoided (by either using a right conjugation action, or a left exponential notation).

While I am, in principle, opposed to bad notations even if they are standard, I'm not familiar with all of the reasons behind the postfix notational choice for substitutions. Thus, being unable to make an educated decision whether the notation should be avoided even if standard, I'll leave it to your discretion whether to introduce and use the postfix notation or not.

A notation differentiating between $\theta$ (on variables) and its completion $\theta^{\ast}$ (on words) might help disambiguate the meaning of $(C_R \theta)^{\ast}x$, if that is indeed what was meant by $x(C_R\circ \theta)$.

[Hernan Ibarra]

small issue: appendices are referenced as sections (e.g., Section A rather than Appendix A). I will submit a PR soon with the fix.

EDIT: PR link

[Hernan Ibarra]

Pace Nielsen said:

Page 24, line 4. Change M= (M,+) by replacing the first M with a script M. A similar change to M=(M,\cdot) should occur three lines later.

I think it's actually meant to be a non-script M unless I'm misreading. I'm fixing the typos you found too.

[Hernan Ibarra]

Pace Nielsen said:

Page 33. In the phrase "that violated E eventually succeeded", should E be replaced by E413?

That whole paragraph seems a bit off, in particular there is an odd reference to E10 which I do not understand. I think it requires clarification.

[Cody Roux]

Pace Nielsen said:

Cody, thanks for the clarification. (And apologies if my wording came across aggressively!)

No harm done :slight_smile:. My heart always leaps in my throat when I think I've made a mistake (I proved this in Lean though!)

Using "weakly collapsing" (with no parentheses) seems like a good choice.

I agree.

There is another place where symbol reversal is very common--- the conjugation notation $a^g =gag^{-1}.$ This leads to some very "funky" looking equations that could be completely avoided (by either using a right conjugation action, or a left exponential notation).

While I am, in principle, opposed to bad notations even if they are standard, I'm not familiar with all of the reasons behind the postfix notational choice for substitutions. Thus, being unable to make an educated decision whether the notation should be avoided even if standard, I'll leave it to your discretion whether to introduce and use the postfix notation or not.

Well, here it's really the function application notation that's wrong! It clashes with the A -> B notation. I'm not proposing we change that though :grinning:. I'll make a jugement call.

A notation differentiating between $\theta$ (on variables) and its completion $\theta^{\ast}$ (on words) might help disambiguate the meaning of $(C_R \theta)^{\ast}x$, if that is indeed what was meant by $x(C_R\circ \theta)$.

I need to double check when I get home, but yes this is what I meant I'm pretty sure. I agree with the notation change. I guess rewriting theorists do hide a lot in there...

[Terence Tao]

@Cody Roux Do you plan to send a PR to implement whatever changes you can make to address Pace's concerns? If so let me know if there are any remaining items that then need to be taken care of.

[Cody Roux]

Yes, and will do, thanks!

[Cody Roux]

@Pace Nielsen I guess in retrospect I was a little terse with my explanations. Indeed you need a second induction to prove $C_R(t\theta) = R(t(C_R\circ\theta))$. And indeed $C_R\circ\theta$ is the substitution that is induced by the composition of functions.

At the time my head was in it, so it seemed more evident.

[Cody Roux]

@Terence Tao I'm done with my edits: https://github.com/teorth/equational_theories/pull/1356

@Pace Nielsen I think I addressed your main points, though you might want to take a quick look before (or after) it's merged.

[Stanley Burris]

Page 7: Grobner Page 22: Gröbner
The second spelling is the correct one in Geman.
Page 36: In Theorem 6.8 change "Whenever R weakly" to "Whenever R is weakly"

---

Parentheses to remove:
Page 21: "(E1286) (and its dual (E2301)),"
Page 31: "this operation satisfies (E1110)"
Page 37: "the right-idempotent law (E378)."
Page 46: "(unipotence law (E40)), x ≃ x ⋄ (y ⋄ y) (right-unit squares law
(E11))"

---

Change = to ≃
Page 23: for x = (x ⋄ ((x ⋄ x) ⋄ x)) ⋄ x (E2441) is

---

The phrasing
"Proposition 5.13 (E73 does not imply E4380). The law x ≃ y ⋄ (y ⋄ (x ⋄ y)) (E73) does not imply x ⋄ (x ⋄ x) ≃ (x ⋄ x) ⋄ x (E4380)."
seems too repetitive. Why not
"Proposition 5.13 (E73 $\not{\models}$ E4380). The law x ≃ y ⋄ (y ⋄ (x ⋄ y)) (E73) does not imply x ⋄ (x ⋄ x) ≃ (x ⋄ x) ⋄ x (E4380)."
This also applies to
Page 31: Proposition 5.15
Page 32: Proposition 5.16
Page 39: Proposition 6.12

In the spirit of these remarks, why not add
"(Does E677 $\models_{fin}$ E255 ?)"
to Problem 8.1 on page 44.

[Cody Roux]

Stanley Burris said:

Page 36: In Theorem 6.8 change "Whenever R weakly" to "Whenever R is weakly"

Ach. I'll do it if the PR is still open

[Terence Tao]

I've gone ahead and implemented the above corrections and suggestions.

[Douglas McNeil]

I may have been too close to the section @Hernan Ibarra called out above to know what was obvious and what wasn't; I'll look at revising for clarity after the work week ends (and, God willing, the Jays win.) :baseball:

[Cody Roux]

Haha I actually remember thinking "those mathematicians will think I'm dumb if I write all this detail"

[Stanley Burris]

I have just finished checking the latest version of the paper and find that all revisions are most satisfactory! In general I would say the paper is quite smooth to read, and should be well received. A big thanks to Terry Tao for creating this project.

The only remaining thing I was considering was to try to present a consistent, coherent commentary on how to use the three kinds of equality, namely =, :=, and ≃, but I think that might be trying everyone's patience to the extreme.

So with a big thanks to everyone for their contributions and for letting me participate, I look forward to the final product, seeing it published and seeing its impact on the mathematical community. I have kept a small group of leading universal algebraists informed, and they have thanked me for giving them an insight into the world of large scale collaborative math projects. With best wishes to all, Stan Burris.

[Shreyas Srinivas]

One small note about my affiliation. I noticed that someone has edited mine to append the segment I inserted into the acknowledgements (about the doctoral student at the Saarbrücken graduate school of computer science)into my full affiliation.

I know this sounds confusing but in the current institutional and legal setup, I would get into trouble if my affiliation looked like that. Adding the graduate school bit in the acknowledgements section is the currently accepted practice that meets a bunch of apparently contradictory regulatory requirements.

[Shreyas Srinivas]

See another example : https://arxiv.org/pdf/2301.05073

[Terence Tao]

Ah, OK, thanks for the explanation. I have separated the affiliations.

[Aaron Hill]

I noticed that the comments about including 'Unaffiliated' were removed in https://github.com/teorth/equational_theories/pull/1330/commits/db313a795c63c67167b6e2019599ea6197bf3a51 . Should I edit my contribution line to remove 'Unaffiliated'?

[Terence Tao]

Hmm, this is a good question, I don't have a strong opinion either way, but I guess we do need to be consistent. I'll set up a poll, but feel free to weigh in as a comment also.

[Terence Tao]

/poll How should unaffiliated co-authors report their status?
By explicitly stating "unaffiliated"
By omitting any mention of affiliation
Other

[David Michael Roberts]

Please note that some publishers/journals require something in the affiliation line (Springer's production company insisted on even adding a city to my employer in my affiliation, when it is a distributed company with people working all over the place and so left that out)

[Hernan Ibarra]

I've added a couple of options to the poll I see are also common practice

[Shreyas Srinivas]

Terence Tao said:

Ah, OK, thanks for the explanation. I have separated the affiliations.

Is this already in the main repository? I don’t see it in the paper. It’s important that the graduate school thing appears in the acknowledgements and not in the main affiliation list to my employer CISPA. Further, since the acknowledgments appear in a different page, I need the footnote indicating the acknowledgments to please the graduate school.

[Douglas McNeil]

I don't have a real preference, although I do think explicitly saying "Unaffiliated" has a kind of punk energy I appreciate.

What really matters is that our songs are fire the results are sound, and our Erdős numbers are lowered to 3. #unaffiliated :sunglasses:

[Hernan Ibarra]

I feel like "independent researcher" also sounds kind of badass ngl

[Terence Tao]

Shreyas Srinivas said:

Terence Tao said:

Ah, OK, thanks for the explanation. I have separated the affiliations.

Is this already in the main repository? I don’t see it in the paper. It’s important that the graduate school thing appears in the acknowledgements and not in the main affiliation list to my employer CISPA. Further, since the acknowledgments appear in a different page, I need the footnote indicating the acknowledgments to please the graduate school.

Oops, forgot to merge, should be good now.

[Terence Tao]

Vaguely related: is anyone in contact with @Fan Zheng ? I have not been able to reach them.

[Jose Brox]

Hernan Ibarra ha dicho:

I feel like "independent researcher" also sounds kind of badass ngl

Idk, I get the feeling that yeti hunters also call themselves independent researchers :speak_no_evil:

[Cody Roux]

Yetis being some kind of magma representation of course. :)

[Pace Nielsen]

I finished reading through the paper, which was very educational! Here are the rest of my (all minor) suggestions:

p. 24, paragraph preceding Example 5.2. In two places, replace \subset with \subseteq.

p. 36, Definition 6.7, second bullet point. Replace \varphi with \varphi_{\theta} in one place.

p. 36, Definition 6.7, fourth bullet point. Replace R(w\theta) with R(\varphi_{\theta}w) in one place.

p. 36, Theorem 6.9. When observing that r is a sub-word of l, it might be helpful to add "since R is weakly collapsing and a weak canonizer".

Also, technically speaking, there is nothing in the definitions to prevent R from being the trivial map and from l=r. So we don't know that r is a proper sub-word. This can be easily handled a number of ways. For instance, we could break into cases, and handle the trivial case l=r separately. Or a nontriviality hypothesis could be added somewhere. Or the implicit assumption l\neq r could be added to a definition somewhere. I personally prefer the first option; just handle the trivial case separately.

p. 37, phrase "from the above equality". Is this the equality in Definition 6.6(2), or some other equality? This should probably be specified.

p. 38, in one place \tilde{w} \to_E \tilde{w} appears, but the first term should have a dash on it.

p. 41. There is a big space after "i.e." (in the Equational Reasoning" paragraph) probably from a missing backslash after the period.

p. 50. Should "in the table below" be changed to "in Table 3" (especially since Table 2 is also below, currently?)

p. 56. In question (2), the phrase "no finite models" should probably be "no nontrivial finite models"

Also, I'd be a bit surprised if question (4) is open.

p. 57. In the string of inequalities

$$\ast < \ast\diamond \ast < \ast\diamond (\ast\diamond \ast) < (\ast\diamond \ast)\diamond \ast$$

if we add

$$< \ast \diamond (\ast \diamond (\ast\diamond\ast)) < \ast \diamond ((\ast\diamond \ast)\diamond \ast)<\cdots$$

this demonstrates the need for the third bullet point. If we include that last \cdots, the words "for instance" at the start of the sentence can be removed.

p. 58, line preceding (E1). I recommend removing u,v and 4,5,\cdots since these do not appear. (If we keep the \cdots, then a \cdots should be added to the list x,y,z,w,\cdots)

End of the paper: Should the "Todo list" be removed?

Penname: I go by "Pace P. Nielsen".

[Terence Tao]

Thanks! I implemented these changes except for the one from p.37 about what "from the above equality" is as I was unsure, perhaps @Cody Roux can weigh in on this one.

[Shreyas Srinivas]

Is it relevant to point out where equational theories find use? Off the top of my head Dolev Yao protocols are equational theories for symbolic reasoning about the security of communication protocols at a certain level of abstraction

[Cody Roux]

@Pace Nielsen @Terence Tao "the above" means the one that was just introduced as an example, namely $y\diamond(x\diamond (y\diamond(y\diamond y))) = x$, I though it would be clunky to name it, but I can change that if it's indeed unclear (note, this is Equation 477 if someone else is going in to change this).

I also agree that I didn't handle the case where $l$ is identical to $r$, which I thought was excluded by my hypotheses but I guess not. I guess the proof of 6.8 could begin with a (very mathy!) "wlog, we assume $l$ is not syntactically identical to $r$..."

[Cody Roux]

@Shreyas Srinivas do mathematical papers traditionally justify the utility of their object of study?

Equational reasoning is an extraordinarily common form of reasoning, not sure we need to talk about Dolev Yao.

[Alex Meiburg]

I think pointing to "this is one/a few standard references on equational theories" could be fine, but yeah I think trying to justify with some application will sound really flimsy.

[Shreyas Srinivas]

That’s the thing. This paper is aimed at the math audience but could just as well be aimed at theoretical computer scientists who don’t work in the verification area and could benefit from mass collaboration on their open problems. In TCS (at least algorithms) it is conventional to mention the relevance of the problem in the beginning in an introduction section unless the problem is so fundamental (like max flow in finite graphs) that everybody knows where it is used.

[Shreyas Srinivas]

For the math audience it probably makes no sense. The few math papers I read (typically graph theory or combinatorics) never have this introduction section.

[Alex Meiburg]

I guess I view "which equations imply which equations" as comparably fundamental and obvious in application to "max flow in a finite graph", myself

[Terence Tao]

I've added a reference to Dolev-Yao in a footnote (and also clarified the equation reference as per Cody's response).

[Shreyas Srinivas]

I want to clarify that Dolev-Yao is just one example that occurred to me because I have interacted with the cryptology community (and Danny) and they use it. There are bound to be other uses.

[Cody Roux]

SMT solvers spring to mind: almost every theory is a pure equational one, arithmetic being the main exception.

[Terence Tao]

I've now moved the mention of Dolev-Yao to the following sentence in the intro: " Equational theories are one of the simplest non-trivial examples of a theory in the model-theoretic sense; they also arise in various areas of computer science, such as term rewriting systems \cite{term-rewriting}, automated theorem proving \cite{mccune-survey}, and in the Dolev--Yao model \cite{dolev} of interactive cryptographic protocols."

[Terence Tao]

The poll has given a slight preference for "unaffiliated", so I propose that I add "unaffiliated" to the six authors who currently do not have a declared affiliation (which would, ironically, make "unaffiliated" the organization with the largest number of coauthors to the project). If any of these authors have reservations about this, please let me know (by DM).

[Kevin Buzzard]

In some sense I think that the fact that unaffiliated people can make nontrivial contributions to a research project is something worth advertising!

[Vlad Tsyrklevich]

@Nicholas Carlini I noticed your name was not in the contributors list. Just wanted to remind you as time is running out.

[Nicholas Carlini]

Hi. Thank you for the ping Vlad. I confess I really don't know what I should do here. I do know that I had a contribution here near the start of this project, and it was quite fun to help you all out. But my hesitation to being actually listed as a contributor is twofold: (1) my contribution was quite minimal relative to what others did---I wrote some small search programs and did some UI programming for like the first month month of the project, and (2) I don't really feel like I understand the core mathematical results---I get it at a high level, but most of the hard theorems are way beyond me, and in CS at least I generally try not to add myself to papers where I don't understand large parts of it. I don't know, do you think the norms here are sufficiently different from what I'm used to that I'm way off the mark?

[Terence Tao]

We have a contributions matrix at https://github.com/teorth/equational_theories/blob/main/paper/contributions.md in which coauthors list the components of the project that they feel comfortable stating that they had a role in, without necessarily claiming complete understanding of other components of the project. If you would like to pursue that route, you can submit a PR similar to the ones in https://github.com/teorth/equational_theories/pulls?q=is%3Apr+contributions+label%3Acontribution  updating the files contributions.tex, contributions.md, and main.tex (for the author list) listing the components you are comfortable claiming, but if not, I can add you to the acknowledgments instead (there are one or two other contributors who have also opted for this).

[Terence Tao]

Also, perhaps it is implicit in the above discussion, but if anyone knows someone who contributed significantly to the project but is not currently listed as a coauthor or in the acknowledgments, feel free to point them towards this discussion thread.

[Cody Roux]

@Floris van Doorn How are you feeling about this?

[Emmanuel Osalotioman Osazuwa]

Noticed a grammatical error in the acknowledgment section of the paper and created a PR to update it: https://github.com/teorth/equational_theories/pull/1365

[Nicholas Carlini]

(Thank you those who DM'd me. I have decided to add my name. If others are hesitant, I've at least been persuaded by the argument the contributions section at least allows people to accurately state what they have and have not done and this made me feel better.)

[Vlad Tsyrklevich]

I'm glad--I pinged you because I remembered you did a lot of work on finite model checking early on among other things and I thought your contribution was absolutely worth recording.

[Shreyas Srinivas]

What else remains?

[Terence Tao]

Huh, against all odds, it looks like we are in fact very close to ready to submit, to arXiv at least. From my vantage point I don't see any outstanding items - does anyone else have any remaining items they want to see addressed? If I don't hear anything in a few days then I will submit to the arXiv. (We still need to decide on a journal; it seems we are still fairly evenly split between the two leading candidates of Annals of Formalized Mathematics and Journal of Automated Reasoning, so perhaps we should continue this discussion further.)

[Shreyas Srinivas]

I recommend adding a secondary subject tag from the CS side in the arxiv submission. I also don’t mind handling the submission since I might find the recommendation this will require useful in the coming months

[Douglas McNeil]

I've just about recovered from the weekend loss :baseball: :disappointed: and so I can add more detail as requested above. Probably just a handful of sentences, so I can fit it in tonight or tomorrow. @Hernan Ibarra : we can negotiate back and forth on level of detail in the PR.

[Bruno Le Floch]

AFAIK @Jose Brox is actively working on a section 7.3 on the usage of ATPs.

[Matthew Bolan]

I need to add information about my scholarship I suppose, will try and do this tonight.

[Hernan Ibarra]

Douglas McNeil said:

I've just about recovered from the weekend loss :baseball: :disappointed: and so I can add more detail as requested above. Probably just a handful of sentences, so I can fit it in tonight or tomorrow. Hernan Ibarra : we can negotiate back and forth on level of detail in the PR.

sounds good, feel free to ping me when you open the PR

[Jose Brox]

Terence Tao ha dicho:

From my vantage point I don't see any outstanding items - does anyone else have any remaining items they want to see addressed? If I don't hear anything in a few days then I will submit to the arXiv.

I'm still working on section 7.3 about the practical use of ATPs. I have rerun some experiments that had crossed platforms, performed some new which demonstrate some subtle issues, @Bruno Le Floch has made some nice plots to show the effect of parameter changing, and I have contacted both Michael Kinyon regarding some questions and problems about Prover9-Mace4, and Laura Kovács regarding Vampire's documentation, and Vampire's failure to prove our "hardest proof": Recall that during the Higman-Neumann side project, we found with Prover9 a proof that required several hours -I later reduced the time to 16 minutes... and nowadays I am able to make Prover9 find the proof in 0.5s! In the ETP we couldn't make Vampire produce a proof for this fact, not even giving it 10h in different modes. Now, they have given the problem a shot in Vampire's team, and it turns out they couldn't get the proof either with what they have tried for now, so this seems not to be a fluke.

Apologies for my repeated delays. I'm writing 7.3 right now, let's see if I can finish it during the night (in Spain it is night right now).

[Jose Brox]

Also, we have some negative results on the existence of 677 anti 255 models (e.g. there are no models up to size 11 included, nor to bigger sizes with some extra conditions), that are not collected in either the paper or the blueprint. Where should we include them?

[Terence Tao]

I think we can list them on the 677 blueprint chapter and briefly mention them in the paper.

[Floris van Doorn]

Cody Roux said:

Floris van Doorn How are you feeling about this?

Thanks for the ping, I added myself in teorth/equational_theories#1371

[Pietro Monticone]

Thank you, @Floris van Doorn!

Could you please also update the files contributions.tex and main.tex (especially the author list)?

Once that’s done, I’ll be happy to merge your PR.

[Pace Nielsen]

The open question 5 on page 56 has an easy answer (and perhaps other easy answers that could be discovered using the equation explorer). The implication E2 -> E4 is irreducible. The proof is very easy. First, note that E4 implies any law of the form l=r where the left-most variable of l matches the left-most variable of r. On the other hand, E4 in conjunction with any law not of that form yields E2.

By the way, in the commentary in the equation explorer on E3, the word "exactly" should be removed.

[Terence Tao]

Thanks, I have changed the open question to give this example and ask for more irreducible implications, and updated the commentary as well.

[Bruno Le Floch]

For what it's worth, there are infinitely many examples of irreducible implications: E2⊨E895, E2⊨E26302, E2⊨E5⊨E13, etc.

Boring details

• E2⊨E895 (Boolean group law): assume E⊨E895 and count modulo 2 the number of times each variable appears. If each one appears an even number of times then E⇔E895. Otherwise E⇔E2 since any model of E is a Boolean group, in which E reduces to x=0.

• https://link.springer.com/chapter/10.1007/BFb0013055 gives a single-law $E_n$ characterizing abelian groups of any given odd exponent $n$. For any prime $p$ the implication $E_n\models E_{np}$ is irreducible. Consider an intermediate law E. In any given model of E (which is necessarily an abelian group of exponent $np$), E reduces to a linear equation $k_1 x+k_2 y+\dots=0$ with $k_i\in[0,np)$, so that the abelian group has exponent $\operatorname{gcd}(k_1,k_2,\dots)$. It must hold in any abelian group of exponent $n$, so $k_i$ are multiples of $n$ and the gcd is either $n$ or $np$.

• E2⊨E26302 (natural central groupoid law) is irreducible for a similar reason to E2⊨E895: natural central groupoids are characterized by the set of idempotents and any further equation either holds in any natural central groupoid or forces the set to be trivial.

• The implication E5⊨E13 is irreducible. Actually, we have the stronger property that E2⊨E13 is next-to-irreducible in the sense that any law E with E2⊨E⊨E13 must be equivalent to E2, E5, or E13. Indeed, E13 states that x◇y=S(y) with S(S(y))=y. Evaluating both sides of E using these identities gives one of x=y, x=S(y), x=x, or x=S(x), in which cases E is equivalent to E2, E2, E13, and E5, respectively. Of course the same properties hold with E13 replaced by E62 (stating that x◇y=S(y) with S a bijection of order 3) or similar equations involving S of prime order. And there are whole families of implications that are next-to-next-to-irreducible, etc.

[Douglas McNeil]

@Hernan Ibarra : at your convenience.

[Shreyas Srinivas]

Where do we stand now? Any pending PRs that need to be merged in?

[Shreyas Srinivas]

And do we have all our contributors on board?

[Shreyas Srinivas]

Also I don’t know how it works in math, but in CS we usually briefly describe our specific contributions and sometimes a one sentence summary or a bulleted list of what is in the paper itself. We also keep it self contained. For example, I’d describe the ETP in one or two sentences before saying what we achieved in terms of number of equals. I was wondering whether we should rewrite it a bit.

[Terence Tao]

Are you referring to individual contributions, or the total contribution of the paper itself? For the former, we are using the contribution PRs to track this, but we could add a link to this in the paper perhaps. For the latter, usually in math we rely in the abstract for this, but we could also add some text at the beginning of the introduction; do you have some proposed text on this that you could PR or suggest here?

[Shreyas Srinivas]

I am talking about the technical contributions of the paper as whole, not that of individual contributions. I have a sample for the initial text below (composed in a bus on a phone).

The Equational Theories project was a mathematical project aimed at resolving the relationships between 4694 equations of 2, 3, or 4 variables. Additionally it was an academic experiment in organising large scale mathematical collaborations using interactive and automated theorem provers. In this paper, we report on our processes and the results of this project. Concretely,

1. We managed to resolve all 22 x 10^6 pairs of equations.
2. Additionally we managed to resolve all but one pairs of equations when only finite models are allowed for refuting an implication.
3. We also developed a suite of techniques for resolving such implications using a combination of heuristics and automated theorem provers and verified the results in lean
4. We developed a collection of tools and techniques to organise and visualise the project and track its progress, which we believe will serve as a useful template for such projects in the future.
   

[Bruno Le Floch]

The current status AFAIK is that all the text is written except Jose Brox' section 7.3. He didn't quite manage to finish it a couple of days back, and had some teaching to do and other real life events to attend to, near the end of this week. We may not hear from him before Monday I think.

[Hernan Ibarra]

Douglas McNeil said:

Hernan Ibarra : at your convenience.

lgtm! much clearer now, thanks.

[Hernan Ibarra]

Shreyas Srinivas said:

Where do we stand now? Any pending PRs that need to be merged in?

Rather than we having to ask every so often, can we come up with a final todo list and keep track of that?

• [x] Douglas McNeil: rewrite modifying magmas section
• [ ] Jose Brox: finish section 7.3
• [ ] All: decide whether to list technical contributions of paper in introduction.
• [ ] etc...

[Hernan Ibarra]

Shreyas Srinivas said:

I am talking about the technical contributions of the paper as whole, not that of individual contributions. I have a sample for the initial text below (composed in a bus on a phone).

The Equational Theories project was a mathematical project aimed at resolving the relationships between 4694 equations of 2, 3, or 4 variables. Additionally it was an academic experiment in organising large scale mathematical collaborations using interactive and automated theorem provers. In this paper, we report on our processes and the results of this project. Concretely,

1. We managed to resolve all 22 x 10^6 pairs of equations.
2. Additionally we managed to resolve all but one pairs of equations when only finite models are allowed for refuting an implication.
3. We also developed a suite of techniques for resolving such implications using a combination of heuristics and automated theorem provers and verified the results in lean
4. We developed a collection of tools and techniques to organise and visualise the project and track its progress, which we believe will serve as a useful template for such projects in the future.

fwiw i really like this outline and would be happy for it to be included in the paper.

[Bruno Le Floch]

I've just submitted the PR https://github.com/teorth/equational_theories/pull/1382 with misc changes to the paper.

There are still 9 bibtex warnings, and many underfull/overfull warnings

There is a stray comment in paper/project.tex, should it just be deleted, or should the text be put somewhere in paper/metatheorems.tex?

\begin{comment}
-- The below should be in the metatheory section.

Use of transitive reduction etc.\ to keep the  \emph{Lean} codebase manageable. Note that the project is large enough that one cannot simply accept arbitrary amounts of  \emph{Lean} code into the codebase, as this could make compilation times explode. Also note somewhere that transitive completion can be viewed as directed graph completion on a doubled graph consisting of laws and their formal negations.
\end{comment}

[Pietro Monticone]

Bruno Le Floch said:

I've just submitted the PR https://github.com/teorth/equational_theories/pull/1382 with misc changes to the paper.

Reviewed and merged.

[Shreyas Srinivas]

Hernan Ibarra said:

Shreyas Srinivas said:

Where do we stand now? Any pending PRs that need to be merged in?

Rather than we having to ask every so often, can we come up with a final todo list and keep track of that?

Given the linear display of messages in a message based platform I think we will inevitably have some repetition of this question. But I understand that we are waiting for @Jose Brox who has time constraints but will be able to finish section 7.3 (about ATP usage). I will create the paper tag at that point.

[Shreyas Srinivas]

What’s the status on this? Can we get to submitting it by the end of this week?

[Jose Brox]

Hi all!

Thank you for patiently waiting for my contributions. I want to report and seek your advice: I have worked hard and long on the ATP's usage section, which is not finished yet, but is in good shape to be finished in a couple of days (what is not yet developed is written in draft-schematic mode).

The section is arising as I envisioned it, but I fear that you may deem it as too long: currently it has 17 pages (with several figures), of which 12 are completely developed. Hence I want to collect your opinion, before keeping on and (hopefully not) finding in the end that you completely dislike the result. Take into account that quite a bit of our hints, tips, and evidence would appear in what remains (as can be seen by looking at the draft).

I attach here the section file (I think it should be a section now, not a subsection), so that you can read it (up to section 1.2.3 at the end of page 12) and decide: Do you like it as it is/would be when finished? Do you want to crop it significantly and you know how? Do you think the best option is just to discard it altogether? @Terence Tao's opinion especially needed here.

ATPs usage.pdf

[Jose Brox]

I should add that I'd really need the paper to be published in arXiv before December 11, because I have a life-or-death application deadline that day (a bold request I know, with me being the main reason the paper is not published yet :smile: )

[Terence Tao]

This is all good reference material, but perhaps is indeed a bit lengthy for the paper as many of the readers may not be so interested in the precise technical features of each ATP, but rather the general performance and lessons. One compromise might be to have some version of the current ATP draft uploaded to the repository somewhere, and a summarized version focusing mostly on performance of the various ATPs we tried on ETP problems, the different strategies used (with that nice graph on page 13), and general "hints and tips"; the operational notes can then be much more briefly summarized, with a link to the longer version in the repo provided for technical details. Given that we can still keep working on the paper even after it is arXiv'ed (and have a delay between arXiv'ing and submitting), we can focus on splicing in a condensed version of the section along the above lines that is presentable (no glaring errors in grammar or missing material etc.) but polish it a bit more later. In particular the longer version can afford to be in draft form for a few more weeks I think even after we arXiv the main paper.

[Alex Meiburg]

I'd something like that. I think about how, several times I think I've seen this in theoretical CS, the only published version of a paper is a "proceedings version" that's at some tight length limit and omits many proofs; and the understanding is to go look at the arxiv version (or maybe even a draft hosted on the author's website!) for the actual full proofs.

[Alex Meiburg]

My point being, I would feel comfortable personally having there be a "repo version" that can happily go into as much depth and appendices as we might like, and a more "camera-ready version" that tries to explain the main points and hit the main notes clearly.

[Douglas McNeil]

We're down to one week before 11 Dec.. @Jose Brox : anything we can do to help, assuming we go the "abbreviated version in the paper, full ATP usage doc in the repo" route?

[Shreyas Srinivas]

Yeah. Arxiv uploads can take a week to get processed.

[Shreyas Srinivas]

We ideally ought to upload the paper tomorrow for this dec 11 deadline to work.

[Shreyas Srinivas]

Is anyone who worked with Jose willing to fill in using the material he has provided?

[Bruno Le Floch]

Why tomorrow? https://info.arxiv.org/help/availability.html suggests the strict deadline would be Wednesday Dec 10, 2pm Eastern time. Of course we shouldn't cut it too close, since it seems important that this last subsection be vetted.

@Jose Brox told me earlier today that he should be done some time today... Let's see if he replies here.

[Shreyas Srinivas]

My memory is that arxiv takes some time to publish it online which can be upto a week

[Bruno Le Floch]

I've never had any delay beyond the standard schedule stated at https://info.arxiv.org/help/availability.html (modified in a predictable way during holidays). It may depend on seniority of the authors, which shouldn't be a problem here, and on the archive.

[Nicholas Carlini]

(Like 95% of the papers I've submitted to arxiv are released exactly on schedule. The remaining 5% that require manual review are because they contain Naughty content and are flagged for manual review, which could always happen but seems unlikely here.)

[David Michael Roberts]

If LLMs and/or AI are mentioned as being used for this research, then my (uninformed) guess is that this paper might be flagged for manual review.

[Jose Brox]

Terence Tao ha dicho:

This is all good reference material, but perhaps is indeed a bit lengthy for the paper as many of the readers may not be so interested in the precise technical features of each ATP, but rather the general performance and lessons. One compromise might be to have some version of the current ATP draft uploaded to the repository somewhere, and a summarized version focusing mostly on performance of the various ATPs we tried on ETP problems, the different strategies used (with that nice graph on page 13), and general "hints and tips"; the operational notes can then be much more briefly summarized, with a link to the longer version in the repo provided for technical details.

Thanks for the kind answer and the (heroically failed!) sanity check :smile: .

Now I have produced a new, abridged version, in which 1) I have removed all technical features and operational notes (this in particular implies that we talk a lot less about Vampire), and 2) I have maintained and expanded the performance data, strategies used, ETP examples, and hints and tips (mainly for Prover9-Mace4).

It is 9 pages long, including several figures (plots, tables). Thanks to @Bruno Le Floch for elaborating four nice graphs! There still are a couple of paragraphs that could be removed without much effort, but otherwise I wouldn't be able to reduce it further without comproimising the information I consider relevant. Of course, go ahead if you want to reduce it further, @Terence Tao!

For convenience, instead of producing a PR just yet, I'm attaching here the whole paper with the ATPs usage subsection 7.3 included (so that references and citations appear correctly), and also the tex file for the subsection (together with the graphs files), in case you want to change it.

@Douglas McNeil can you please your lay your sharp eyes on this text too? Last time you were very helpful!

Regarding the longer version, I agree that we can upload it to the repository, and we can even think of publishing it somewhere as some kind of companion guide, if you believe it is worth doing. In any case, I'm prioritizing the publication in arXiv, and will finish the longer version later.

Thanks everyone again for the wait!

ATPs usage.rar
Paper.pdf

[Alex Meiburg]

David Michael Roberts said:

If LLMs and/or AI are mentioned as being used for this research, then my (uninformed) guess is that this paper might be flagged for manual review.

I doubt that. I think that a very large portion of arxiv submissions come from ML (from what I've heard, > 1/3), and probably almost all of those contain phrases like "... ChatGPT generated ..." or "... the LLM says".

[Alex Meiburg]

(this doesn't mean we shouldn't get it out soon.) I also have never seen it go past the "regular" deadline.

[Martin Dvořák]

I just opened the PDF after a long time not seeing it, and I noticed that every other page says
EQUATIONAL THEORIES PROJECT CONTRIBUTORS
on the top.

I think it doesn't bring much value. I suggest it should either say "Terence Tao et al." or just "Equational Theories Project" as the other half of pages say.

[Shreyas Srinivas]

Let’s PR this version please (cc : @Jose Brox )

[Shreyas Srinivas]

As soon as everyone agrees, we can merge the PR and create the arxiv v1 tag

[Shreyas Srinivas]

@Martin Dvořák : I think the editors will do their magic or tell us what to do when the submission gets past peer review

[Jose Brox]

Shreyas Srinivas ha dicho:

Let’s PR this version please (cc : Jose Brox )

It's done now!

[Shreyas Srinivas]

I’ll wait for the reviews to come in

[Shreyas Srinivas]

Once the PR is merged. I hope we can figure out how to get everyone to sign off (I.e.agree to submit to arxiv)

[Martin Dvořák]

I don't think it is feasible to wait for each author's approval.

[Shreyas Srinivas]

It’s necessary

[Shreyas Srinivas]

Maybe we create a separate thread where every listed author signs off with a message

[Martin Dvořák]

You can create a "veto" period for the arXiv submission, but if you wait for everybody to opt-in, @Jose Brox will certainly miss his deadline.

[Shreyas Srinivas]

Okay. If reviews come in and we merge the PR today, I’ll do the arxiv submission today or tomorrow.

[Douglas McNeil]

So this is a lesson learned: we should have sorted out how we were going to handle this earlier. Next time. :upside_down: But let me sketch an argument that we're okay submitting tomorrow.

The arXiv policy is that the submitting author agrees

• I am completing this Agreement on behalf of and binding upon all author(s).
• I have full authority to enter into and make this Agreement and to grant the rights contained in this Agreement. If the Work was created by multiple authors, I affirm that my co-author(s) have consented to the submission of the Work to arXiv under the Agreement terms with me acting on my co-author(s)’ behalf.

In large, more hierarchical, collaborations in astronomy, in practice the leader of each subteam typically consents on behalf of everyone they're overseeing. Sometimes paperwork goes out to everyone to positively assent and people get chased down on holidays, etc. In our group that won't work, not least of which is that some of us answer to no one. :sunglasses: The conventions are more sophisticated than you might assume, though, everyone knows that different people did different parts and coauthor G isn't held responsible for mistakes in team R's section.

In our case, everything is public, and every named author (along with everyone else on the planet!) has had an opportunity to follow the development of the paper at whatever frequency they liked. The action of contributing your name to the paper (assuming we added no one without direction) given our public Zulip+github setup is a presumptive consent that you're okay with the expected forward movement of the process, given that at any moment you have the opportunity to opt out.

I do think we should arrange a more formal signoff before submission to a journal proper, given that our submitting author is on the hook for the agreement, but I'd be okay with @-ing all submitters ASAP giving them a veto period for now. We then require one final positive assent from everyone before journal submission, which we can start as early as possible (maybe following Shreyas' thread idea) to give us the largest window to connect with our less online members.

[Shreyas Srinivas]

We can already start collecting this consent now.

[Shreyas Srinivas]

Can someone create the thread please?

[Shreyas Srinivas]

Just tag everyone and ask them to write a message expressing their consent

[Martin Dvořák]

As for the journal submission, I am worried that some of us might die earlier than we get the last assent. However, we should at least have a longer veto period (maybe 3 months or so) for the journal submission.

[Harald Husum]

I hope it isn't too late. I did a typo checking pass on the paper just now: https://github.com/teorth/equational_theories/pull/1393

[Shreyas Srinivas]

Let’s merge this after Jose’s PR please (@Pietro Monticone )

[Shreyas Srinivas]

I don’t want to create merge conflicts for his section right now.

[Harald Husum]

That makes perfect sense. I'm comfortable with dealing with dealing with any merge conflict on my end.

[Harald Husum]

Please do merge https://github.com/teorth/equational_theories/pull/1392 though. That one shouldn't conflict with Jose's PR.

[Terence Tao]

I did unfortunately create a merge conflict with Jose's PR somehow before seeing this message, but hopefully it is minor and can be fixed.

[Jose Brox]

Jose Brox ha dicho:

It is 9 pages long, including several figures (plots, tables). Thanks to @Bruno Le Floch for elaborating four nice graphs! There still are a couple of paragraphs that could be removed without much effort, but otherwise I wouldn't be able to reduce it further without comproimising the information I consider relevant. Of course, go ahead if you want to reduce it further, @Terence Tao!

Are there any complains regarding the actual content of the section? Any fundamental changes that should be made?

[Terence Tao]

I think it looks like a good overview of the state of the art. It may still be that a referee may want to trim some of the more technical information, but I think it's basically ready to be merged and then the paper submitted, once the various typos pointed out in the PRs (as well as the merge conflict) are resolved.

[Shreyas Srinivas]

okay.
@Jose: Let me know when the typos are fixed. I will merge the PR.

To all : I will also ping here for getting the arxiv nomination from someone. I imagine this paper will fit in at least on math tag related to universal algebra, and one CS tag related to formal methods. Please let me know the best choices here

[Bruno Le Floch]

I suspect it's not quite realistic to submit in the next 63min, see https://arxiv.org/localtime . The following arXiv deadline is in 73 hours, which would make the paper appear on (Monday Dec 8 night)/(Tuesday Dec 9 morning), still perfectly fine.

[Shreyas Srinivas]

We can always make the submission a bit early

[Shreyas Srinivas]

But let’s wait for the reviews and approvals

[Harald Husum]

I made another tidying PR: https://github.com/teorth/equational_theories/pull/1394

This is really scraping the barrel now.

[Martin Dvořák]

I don't know the context of this paragraph, but is
image.png
intentional?

[Terence Tao]

Do you have any more information about the source of this image? I did a text search but could not find it in the repo.

[Martin Dvořák]

It was Example 7.1. in the PDF from "Paper sign off". I don't see it in the current version tho. So I guess all good?

[Cody Roux]

We should probably leave 1 or 2 things for the reviewers to catch, as nourishment :grinning_face_with_smiling_eyes:

[Martin Dvořák]

BTW we currently have a mix of — surrounded by spaces and the same symbol—not surrounded by spaces.
Would you mind if I unified it to have\,---\,surrounded by tiny spaces everywhere?

[Terence Tao]

Martin Dvořák said:

It was Example 7.1. in the PDF from "Paper sign off". I don't see it in the current version tho. So I guess all good?

Ah, OK. I think this is intentional, introducing a new operation / to witness injectivity. It should be part of a larger PR (currently held up due to a merge conflict).

[Martin Dvořák]

Martin Dvořák said:

BTW we currently have a mix of — surrounded by spaces and the same symbol—not surrounded by spaces.
Would you mind if I unified it to have\,---\,surrounded by tiny spaces everywhere?

I would also be fine with a half of the \, space on each side.

[Terence Tao]

Martin Dvořák said:

Martin Dvořák said:

BTW we currently have a mix of — surrounded by spaces and the same symbol—not surrounded by spaces.
Would you mind if I unified it to have\,---\,surrounded by tiny spaces everywhere?

I would also be fine with a half of the \, space on each side.

Sure, this is fine with me, although this is also the type of change that can safely be done between arXiv submission and any referee reports, so no rush.

[Martin Dvořák]

Terence Tao said:

Sure, this is fine with me, although this is also the type of change that can safely be done between arXiv submission and any referee reports, so no rush.

My perfectionism won over any common sense I could have had:
https://github.com/teorth/equational_theories/pull/1395

[Harald Husum]

Cody Roux said:

We should probably leave 1 or 2 things for the reviewers to catch, as nourishment :grinning_face_with_smiling_eyes:

I think it is a good idea to leave as few trivial issues for reviewers to catch as possible. The less trivial stuff there is for a reviewer to comment on, the more they are forced to dive more deeply into the issues we want then to look at.

I say this, based on the assumption that peer review has a lot in common with the PR review in software development, which might or might not be the case.

[Jose Brox]

Martin Dvořák ha dicho:

I don't know the context of this paragraph, but is
image.png
intentional?

Yes, that is in fact intentional: this is defining, in Mace4 language, a new operation "\" that encapsulates the fact that the left multiplication map (for operation *) L_{S(x)} is injective. It should still appear in Example 7.1, if everything is well.

[Jose Brox]

Martin Dvořák ha dicho:

My perfectionism won over any common sense I could have had

This sentence encapsulates my entire life :sunglasses: :melting_face:

[Jose Brox]

Shreyas Srinivas ha dicho:

To all : I will also ping here for getting the arxiv nomination from someone. I imagine this paper will fit in at least on math tag related to universal algebra, and one CS tag related to formal methods. Please let me know the best choices here

Who could be able to endorse @Shreyas Srinivas in arXiv?

[Terence Tao]

I should be able to endorse for math at least; I don't know about CS.

[Shreyas Srinivas]

If I correctly recall the endorsement process I need to start the submission and get some link and code.

[Shreyas Srinivas]

And Jose said something like this in DM as well.

[Jose Brox]

Shreyas Srinivas ha dicho:

okay.
@Jose: Let me know when the typos are fixed. I will merge the PR.

It is done now! Project started building.

[Shreyas Srinivas]

In CS, the topic is "Logic in Computer Science" or "PL". More likely the former

[Bruno Le Floch]

One thing I'm not sure about is that we cite repositories like leanblueprint both as footnotes with the url (footnote 8), and as references in the bibliography (ref [41]). We also refer to our repository as [13], with a stale list of authors. Which way should we prefer? EDIT: I just realized our repository's author list could in principle be different from the paper's author list for good reasons, but I have no way of determining the correct one.

(I will submit tonight (in ~14 hours) a PR with such fixes and any typo I find when reading section 7.)

[Jose Brox]

@Shreyas Srinivas I have sent a PR to re-include a citation that I removed somehow.

[Shreyas Srinivas]

I merged that PR and the typo fixes.

[Shreyas Srinivas]

Shall I start submission?

[Shreyas Srinivas]

I'll send DMs for endorsement. Since universal algebra is in "Rings and Algebras", that's what I need an endorsement for first

[Jose Brox]

I believe @Bruno Le Floch wanted to make a final review, look for typos, etc.

[Shreyas Srinivas]

I want to test arxiv's acceptance of the latex side. I need to tell it to use xelatex right?

[Shreyas Srinivas]

I'll also start getting the endorsements

[Jose Brox]

I was also producing a more refined version of the other max_weight plot, I think it needs around 30 minutes more (although it is not essential).

[Shreyas Srinivas]

Good news : the arxiv submission works smoothly. Just let me know when CI shows build complete on the main branch after all the processing is done.

[Shreyas Srinivas]

I'll tag and upload the latest files at that point and finish submission. Preferably in the next few hours.

[Jose Brox]

PR created with new image.

[Harald Husum]

I noticed that we use a mix of date formats in the paper. Is this worth standardizing?

Currently we use [Month DD, YYYY], [DD Month, YYYY] and [YYYY-MM-DD] in different paragraphs.

[Martin Dvořák]

I am voting for YYYY-MM-DD.
https://en.wikipedia.org/wiki/ISO_8601

[Harald Husum]

For what it is worth, I tasked Claude Opus with peer reviewing the paper in its current form. I'll share the resulting report here. Take the content with the usual LLM-sized grain of salt, but also do feel free to act on this if anything stands out as important to you.

Peer Review Report: Equational Theories Project Paper

Issues Ranked by Severity

---

HIGH SEVERITY (Correctness Issues)

1. Incorrect equation in ml.tex (line 3)

- Issue: The law $\Eq{1659}$ is stated as "$\x \op ((\y \op \y) \op \z) \formaleq \x \op y$" but the correct form per numbering.tex is "$\x \formaleq (\x \op \y) \op ((\y \op \y) \op \z)$"
- Note: The y at the end is also missing the backslash (\y)
- Location: paper/ml.tex:3

2. Missing \times M in variety definition (constructions.tex:52)

- Issue: The variety for the idempotent law is written as "$ (a,b) \in M: a+b=1 $" but should be "$ (a,b) \in M \times M: a+b=1 $" for consistency with the preceding examples
- Location: paper/constructions.tex:52

3. Inconsistent variable notation in Examples (constructions.tex:49, 56, 58)

- Issue: Uses x, y, z instead of \x, \y, \z which are used consistently elsewhere in the paper. This creates visual inconsistency.
- Location: paper/constructions.tex:49, 56, 58

---

MEDIUM SEVERITY (Inconsistencies/Uncertainties)

4. Inconsistent counts: "820 or 822" vs "820"

- Issue: intro.tex states "either $820$ or $822$" pairs while austin.tex says definitively "$820$ new implications". Similarly for the anti-implications: intro.tex says "$13854535$ or $13854537$"
- Impact: This uncertainty about final counts undermines confidence in completeness
- Location: paper/intro.tex:134, 144 vs paper/austin.tex:5

5. Missing \Cref for subsection reference (constructions.tex:305)

- Issue: Uses \ref{greedy-sec} instead of \Cref{greedy-sec} which is used consistently elsewhere
- Location: paper/constructions.tex:305

6. Inconsistent appendix references (higman.tex:28)

- Issue: Uses "Appendix \ref{numbering-app}" while intro.tex uses \Cref{numbering-app} consistently
- Location: paper/higman.tex:28

---

LOW SEVERITY (Bibliography/Minor Issues)

7. Duplicate bibliography entry for Sheffer

- Issue: Both @article{sheffer,...} (line 137) and @article{sheffer1913set,...} (line 219) reference the same 1913 Sheffer paper. Only sheffer appears to be cited.
- Location: paper/references.bib:137, 219

8. Missing year in bibliography entry

- Issue: The githubGitHubPatrickMassotleanblueprint entry has year = {}, (empty)
- Location: paper/references.bib:958

9. Unusual/non-standard citation key naming

- Issue: githubGitHubPatrickMassotleanblueprint and GitHubGitHubPatrickMassotleanblueprint appear to be the same but are cited differently in project.tex (uses the capitalized version which doesn't match the bib entry exactly—though

BibTeX is case-insensitive, this is confusing)

- Location: paper/references.bib:954, paper/project.tex:20

---

SUGGESTIONS (Not Errors)

10. Future dates in paper

- The paper references dates like "July 30, 2025" (project.tex:60 figure caption) and "22-09-2025" (references.bib). If this paper is to be published before these dates, consider whether these should be updated.

11. Equations used but not defined in numbering.tex appendix

- Several equations are referenced via \Eq{n} notation (e.g., $\Eq{14}$, $\Eq{492}$, $\Eq{1090}$, $\Eq{1482}$, $\Eq{1523}$, $\Eq{1682}$ in spectrum.tex) that are not listed in the appendix's equation table. While the \Eq{} macro just

renders as "En", having these in the appendix would aid readers.
12. Higman-Neumann section not formalized

- The section explicitly states the results "have not been formalized in Lean yet" (higman.tex:54). This is appropriate disclosure but worth noting as a limitation.

---

Summary

The paper is generally well-written with clear mathematical exposition. The most significant issues are:

1. The incorrect equation form for $\Eq{1659}$ in the ML section
2. The uncertainty in final counts (820 vs 822, etc.)
3. Minor typographical inconsistencies in variable notation

These should be addressed before publication. The bibliography issues are minor cleanup items.

[Jose Brox]

Harald Husum ha dicho:

1. Incorrect equation in ml.tex (line 3)

- Issue: The law $\Eq{1659}$ is stated as "$\x \op ((\y \op \y) \op \z) \formaleq \x \op y$" but the correct form per numbering.tex is "$\x \formaleq (\x \op \y) \op ((\y \op \y) \op \z)$"
- Note: The y at the end is also missing the backslash (\y)
- Location: paper/ml.tex:3

This indeed is a mistake. I have followed the ChatGPT link, and the equation actually is
$xy = x((yy)z)$, so its correct number is 3523.

Harald Husum ha dicho:

2. Missing \times M in variety definition (constructions.tex:52)

- Issue: The variety for the idempotent law is written as "$ (a,b) \in M: a+b=1 $" but should be "$ (a,b) \in M \times M: a+b=1 $" for consistency with the preceding examples
- Location: paper/constructions.tex:52

This is clearly true too.

I have added these two corrections to my open PR. Can someone look at the rest? (Gotta go now)

[Bruno Le Floch]

I'll go through the others and include them in my upcoming PR.

[Shreyas Srinivas]

Orthogonal note : The arxiv submission process has drastically improved since early this year

[Bruno Le Floch]

@Shreyas Srinivas Regarding which TeX engine to use, I just checked that our automated pipeline uses pdf(La)TeX, so I think it is better to stick with that rather than XeLaTeX as you had mentioned upthread.

[Shreyas Srinivas]

Okay. But fwiw, I did try running xelatex on the arxiv upload service and the output seemed fine. I just have to change the submission now to the one with your PR

[Bruno Le Floch]

Martin Dvořák said:

I am voting for YYYY-MM-DD.
https://en.wikipedia.org/wiki/ISO_8601

@Martin Dvořák I don't know how to efficiently locate all the dates in the paper. I found three on page 1, one in figure 8, and one in the ml section. Are there more? The ISO convention (and YYYY-MM for months) would look ugly in the introduction, no? «[...] project launched in 2024-09 to explore [...]» «The project achieved its primary goal on 2025-04-14, when the 4694×(4694-1) = 22028942 implications [...]»

[Bruno Le Floch]

@Shreyas Srinivas Yes, our paper is sufficiently simple that pdfLaTeX, XeLaTeX and LuaLaTeX should give almost identical visual outputs, but it seems slightly safer to stick with whatever we were using. For my PR I still need a couple of hours of proofreading, plus the incompressible 1 hour of CI. There is also Jose Brox's PR https://github.com/teorth/equational_theories/pull/1400 to account for.

[Shreyas Srinivas]

The CI is still running on that one

[Shreyas Srinivas]

I’ll guessing I can wake up tomorrow morning and finish the upload before catching my train

[Bruno Le Floch]

Yes, although do note there is still 45 hours or so before the next arXiv deadline, so depending on what you're up to afterwards, there may be no rush.

[Bruno Le Floch]

https://github.com/teorth/equational_theories/pull/1401 (CI currently running because I made some last minute commits) The following improvements could still be done, but not by me, and they are not necessary. None of them are blockers for arXiv submission.

• The introduction could point to sections 2, 3, 4, 8, 11, 12, 13 at least to announce what's in them or how the paper is organized. Currently it only announces a few of the sections.
• Footnotes 1, 2 could possibly be replaced by the references [13] and [64]. Footnotes 3, 6, 14, 25, 37, 44 could be turned into references.
• Dates could be normalized to the same format (ISO?).
• The almost vertical arrow in the middle of Figure 4 could be made vertical
• The very slightly jagged horizontal arrow near the top right of Figure 7 could be made straight
• The style of all tables could be streamlined (perhaps Table 1 should be transposed)
• Figure 11: the MagmaEgg example figure could be fixed (see details)
• Figure 16 could be updated to the latest Equation Explorer version
• The points 10-12 in Harald Husum's Claude review could be looked at (my PR dealt with the others, except point 4 which was irrelevant).

[Shreyas Srinivas]

I’ll submit tonight. I have a busy day ahead

[Shreyas Srinivas]

More concretely, the CI is running and there’s already an arxiv submission with all the details filled in. I just have to change the files

[Jose Brox]

Shreyas Srinivas ha dicho:

I just have to change the files

So you already got endorsement then?

[Shreyas Srinivas]

For the math side yes. Arxiv hasn’t asked me to get an endorsement for the secondary tag yet

[Harald Husum]

Here's a final LLM-generated review of the paper as it stands now. This time by Codex:

Review Notes

• Scope of formalization wording (paper/intro.tex:5–47 vs paper/foundations.tex:84; paper/data.tex:3) — Intro/outcomes still say all 22,028,942 implications are “formalized in Lean,” while Foundations and the Data section say only a generating set is formalized and the rest are filled by external programs. In the repo the closure is now computed inside Lean (as a computation, not one theorem per edge) via equational_theories/Closure.lean and scripts/extract_implications.lean. Please harmonize: e.g. “we formalize 10,657 positive and 586,925 negative generators in Lean, and compute the full closure by a Lean program (not external tooling)” or, if some edges remain non-Lean, spell out exactly what is formally verified and what is not.
• Finite-equivalence argument too terse (paper/constructions.tex:117–118) — The remark that Eq 206 and Eq 1648 are equivalent for finite magmas is sketched in one direction and the reverse is “similar.” Because this justifies why the constructions must be infinitary, please either give the full finite-magma proof in both directions or point to the exact Lean/blueprint lemma establishing the equivalence.
• Linear model claim needs correction (paper/spectrum.tex:12–18) — Stating that the linear operation \((a,b)=(1,1)\) “cannot satisfy a law for all \(n\)” is false: addition mod \(n\) satisfies associativity/commutativity uniformly. Please clarify the intended restriction (e.g., “(1,1) only gives the already-covered commutative/group consequences and yields no new full-spectrum witnesses”) or otherwise correct the claim.
• Counterexamples not cited (paper/metatheorems.tex:204–207) — The proof sketch of Proposition \ref{854-3316} rejects cases (i) and (iii) by appealing to counterexamples to \(\Eq{854}\models\Eq{4}\) and \(\Eq{854}\models\Eq{10}\) but provides no model or pointer. Please cite the Lean statements already present: equational_theories/ManuallyProved/Equation854.lean:41 (not_l4) refutes \(\Eq{854}\models\Eq{4}\) and equational_theories/ManuallyProved/Equation854.lean:47 (not_l10) refutes \(\Eq{854}\models\Eq{10}\); both are derived from explicit finite models (All4x4Tables / FinitePoly).
• Ambiguous “constant law” naming (paper/numbering.tex:61–63) — Both \(\Eq{41}\) and \(\Eq{46}\) are labeled “constant law” though they differ (\(x\op x\) vs \(x\op y\)). To avoid later ambiguity when referring to “the constant law,” please either disambiguate the labels (e.g., “diagonal constant” vs “binary constant”) or add a note that both names refer to equivalent laws.

Not sure any of this is worth investigating/addressing before uploading the preprint. Do you have a take @Shreyas Srinivas?

[Shreyas Srinivas]

I need to go over these comments in detail with the pdf. The first point is valid. For the others, I prefer multiple authors to go over them.

[Shreyas Srinivas]

But I think we can handle these in a preprint v2.

[Shreyas Srinivas]

At the moment, we are preprint ready. I think we do have clarifications for point 1 a bit further down. I recall reading it a bit later. Introductory sentences are often sparse in detail. Can someone with access to the pdf confirm this?

[Shreyas Srinivas]

I am on a train right now and the internet connection is unreliable at best.

[Bruno Le Floch]

I think you should submit without addressing these points, which can all wait for the journal submission or a v2.

The first point is partially valid: in the introduction we could potentially be more precise than "formalized in Lean". But I thought that the main text was correct when saying only a generating set is formalized and we don't actually have an end-to-end theorem; did that change? I believe scripts/extract_implications.lean is about packaging data for the Equation Explorer and similar non-Lean tools.

The second point should be ignored: the proof E1648⊨(finite)E206 really is very similar to E206⊨(finite)E1648. We don't point to the specific blueprint lemma for all proofs in the paper.

The third point is a mistake on my part when writing the spectrum section; what happens is that (a,b)=(1,1) can only obey laws whose order on both sides is positive (and of course the empty law 1), which are already covered by (a,b)=(0,0). I'm too tired to find a good short replacement sentence.

For the fourth point (on not(E854⊨E4) and not(E854⊨E10)) we could mention that the E854⊨E4 counterexample is a magma of size 2 and the E854⊨E10 counterexample is a magma of size 11 (minimal, I just checked, and there are many such magmas).

For the fifth point about constant laws, come on, this is abusive pedantry, the laws are equivalent.

[Shreyas Srinivas]

I agree with you about the fifth point. At the same time, we are working on universal algebra and we are formalising stuff and pedantry seems to be a part and parcel of both.

[Shreyas Srinivas]

Anyway, I can’t predict how math reviewers will perceive this since I have no experience with math submissions. I come from CS. If you say it’s pedantic then I accept it.

[Shreyas Srinivas]

About the end to end theorem, I don’t think we proved it in a way free of native_decide. This means for all intents and purposes of this project, we didn’t prove it.

[Harald Husum]

Bruno Le Floch said:

For the fifth point about constant laws, come on, this is abusive pedantry, the laws are equivalent.

I think it is a good sign regarding the health of the paper that this is what the model comes up with, though. So I figure we should take it as some sort of a compliment.

[Harald Husum]

Also, to be clear, I have no intuition at all in terms of when a paper is "good enough". I just found the points listed by Codex to be plausible and wanted some second eyes on them. I don't mind us uploading the preprint without addressing these points, as long as someone more knowledgeable than me are saying that it is fine. I count you as such Bruno.

[Jose Brox]

Oh, looking at the new version of the paper I see that the algorithm in Section 7.3.6, due to a page break, appears now broken in half with two tables in the middle. This is something we should fix in future versions.

[Jose Brox]

In the author contributions appendix, we state that "In a companion document to this paper, the contributions of each author of this paper to the ETP are described". Should we upload this document to arXiv too, or how will we proceed with it?

[Terence Tao]

The lazy thing to do is just supply https://github.com/teorth/equational_theories/pulls?q=is%3Apr+label%3Acontribution+ as the "companion document". Incidentally for some reason there are only 32 PR's marked "contribution" when there are 34 authors. Not sure exactly what the discrepancy is, but I'm sure it can be sorted out (a mislabeling perhaps)? EDIT: Ah, I found two contributing PRs that weren't given the "contribution" label. There might still be duplicates, but at least the numbers match now.

EDIT: After removing one redundant contribution, it appears that @Douglas McNeil should upload a contributions PR still.

[Shreyas Srinivas]

as it happens arxiv will delete contributions.md

[Shreyas Srinivas]

should I go ahead and submit now?

[Douglas McNeil]

Okay, created a PR, although contributions.md was already mostly right anyway.

[Shreyas Srinivas]

the arxiv submission is technically one version before the tag

[Shreyas Srinivas]

I'll fix this now. Thankfully caught it before hitting submit

[Shreyas Srinivas]

This is the last PR before submission

[Shreyas Srinivas]

any mistakes can be corrected in v2 or journal submission

[Shreyas Srinivas]

fwiw, arxiv deletes contributions.md anyway

[Shreyas Srinivas]

The die is cast

[Jose Brox]

Thanks for taking care of this process, @Shreyas Srinivas!

[Bruno Le Floch]

Hm... there was some logic to me writing :a: :r: :x: :info: :check_mark: reacting to the arXiv submission, but I'm missing the joke with :lettuce: :cheese: :back: :knife: :chicken: :not_allowed: Can someone explain?

[Martin Dvořák]

https://en.wikipedia.org/wiki/Alea_iacta_est

[Martin Dvořák]

I first though that :lettuce: :cheese:
https://en.wikipedia.org/wiki/Caesar_salad
would be enough, but then I decided to add more hints.

[Bruno Le Floch]

Ah, thanks! Oh, and :chicken: :not_allowed: is by Jose, not you.

[Martin Dvořák]

We were discussing about whether chicken meat belongs to the Caesar salad or not.

[Jose Brox]

Yes, I was hinting at the lack of chicken in that Caesar salad! For me it is a defining ingredient, but Martin has taught me that the original one didn't have it.

[Bruno Le Floch]

An alternative meaning being that there is no more chickening out of this submission.

[Martin Dvořák]

I don't have any culinary knowledge. Wikipedia says so, however.

[Cody Roux]

The lack of Rubicon emoji is troubling

[Shreyas Srinivas]

Is that what they are signifying by putting chicken in a Caesar salad?

Martin Dvořák said:

I don't have any culinary knowledge. Wikipedia says so, however.

[Shreyas Srinivas]

If so then Jose is correct. Caesar can’t chicken out.

[Jose Brox]

How are we going to share the arXiv author's password? Will you send an email to all authors, @Shreyas Srinivas?

[Shreyas Srinivas]

Yeah. When it arrives

[Shreyas Srinivas]

Or maybe is a big group dm here on Zulip

[David Michael Roberts]

:tada: https://arxiv.org/abs/2512.07087

[Terence Tao]

It seems @Fan Zheng 's name got truncated in the arXiv metadata. It should get changed, but perhaps it can wait a few days so that we can bundle it with any other changes that may need to be made.

[Bruno Le Floch]

I have a few changes upcoming by the end of the week.

[Shreyas Srinivas]

If we want their name to be indexed in Google scholar or dblp, we should probably change it right away.

[Bruno Le Floch]

Can you email the arXiv admins? There is a non-zero chance they can fix this quickly without a v2. Otherwise yes, you're probably right that it has to be resubmitted before tonight.

[Shreyas Srinivas]

I’ll try. But I will be busy for the next two hours. Once the group DM is in, all you will have ownership. If someone volunteers for this I am fine with that too

[Jose Brox]

I have created a formal group called PaperAuthorsETP, but I don't seem to be able to DM the group. Can you see it @Shreyas Srinivas?

[Shreyas Srinivas]

Not yet

[Shreyas Srinivas]

I didn’t know we could name them

[Jose Brox]

In Settings (gear icon at the upper right corner) we have the Group configuration or Group settings option (I see it in Spanish).

[Jose Brox]

David Michael Roberts ha dicho:

:tada: https://arxiv.org/abs/2512.07087

Thank you @all for your understanding and your support! :hug:

[Shreyas Srinivas]

Anyway the group DM doesn’t exist. I’ll tentatively give you an Bruno the password. Once someone can setup the big group DM I’ll share it there too

[Bruno Le Floch]

In principle, all of us should now have the paper password: I've sent a DM to everyone in what seems to be a big group DM

[Bruno Le Floch]

I've contacted the arXiv help desk for Fan Zheng's name. Probably nothing will happen until they start their day in a couple of hours. EDIT: The name got corrected!

[Shreyas Srinivas]

I woke up to the preprint online. I can’t offer you all actual champagne so these virtual emojis will have to do for now. Congratulations :clink: !!

[Shreyas Srinivas]

Now it’s probably time to ping the busy beaver authors and ask them to update their citation.

[Shreyas Srinivas]

Is any of them on Zulip?

[Bruno Le Floch]

Yes, Daniel Briggs, Nathan Fenner, Yannick Forster, Matthew House, Maja Kądziołka, Shawn Ligocki, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann. From their pdf it seems Tristan Stérin is the corresponding author, I'll let you contact him.

[Shreyas Srinivas]

Cc @Tristan Stérin

[Shreyas Srinivas]

Hey we got the paper uploaded to arxiv as promised a few months ago. We would like to request your citation to be updated to point to the arxiv paper.

[Jose Brox]

Terence Tao ha dicho:

(We still need to decide on a journal; it seems we are still fairly evenly split between the two leading candidates of Annals of Formalized Mathematics and Journal of Automated Reasoning, so perhaps we should continue this discussion further.)

Perhaps it is time to decide on a journal? Do you want to open a different thread for this? Are there other suitable options that we should consider, apart from AFM and JAR?

[Tristan Stérin]

Shreyas Srinivas said:

Hey we got the paper uploaded to arxiv as promised a few months ago. We would like to request your citation to be updated to point to the arxiv paper.

@Shreyas Srinivas congratulations to you all!! We're planning on releasing a v2 of our arxiv paper Q2 of next year, after we get our first feedback from peer reviews, are you OK if we wait until that point to update the citation?

[Shreyas Srinivas]

I am not a good judge of what to do here, but I think it would definitely help some of our colleagues who aren't far up the career ladder yet to have that citation sooner, especially since this is application season in many places.

[Tristan Stérin]

Capture d’écran 2025-12-09 à 14.19.52.png
@Shreyas Srinivas this is what we currently have. If we're not missing any authors, I don't think it makes any kind of difference to add the arxiv link now or in 6 months.

[Shreyas Srinivas]

There are 34 authors in our paper. Only 27 are mentioned here

[Shreyas Srinivas]

And it affects the citation count on google scholar for example.

[Tristan Stérin]

Shreyas Srinivas said:

There are 34 authors in our paper. Only 27 are mentioned here

This is important yes. We used the state in which your author list was in mid September.

Also note that that for any actual publication of our paper (which won't happen before 6 months to a year) we will have your latest updated citation.

I'm still personally quite reticent in us releasing a new arxiv version just now. I was wrong and our reviews should actually come back by the beginning of February, which would be then the right moment for us to have enough modifications to warrant a new version on arxiv.

However, I will ask our co-authors what they think and we'll act democratically on that one!

[Shreyas Srinivas]

I think it misses Floris von Doorn, Amir Bar-Livne, Bernhard Reinke, Fernando Vaquerizo-Villar, Hernán Ibarra Mejia, Pace P. Nielsen, and Emmanuel Osalotioman Osazuwa

[Tristan Stérin]

For reference, this is what we used which was up to date with your preprint at the end of Aug:
#Equational > 🦫 BB5 "pre-preprint", feedback phase until June 30th 2025 @ 💬

[Shreyas Srinivas]

I think that’s fair given the info we had back then. We don’t want any of our authors to miss out on the credit for their work, but it also makes sense that your collaborators would also want to make a collective decision, especially since the change is so small.

[Terence Tao]

I wrote a blog post about the paper: https://terrytao.wordpress.com/2025/12/09/the-equational-theories-project-advancing-collaborative-mathematical-research-at-scale/

[Bruno Le Floch]

Oops, the functionality to parse equations in the Equation Explorer is completely broken at present. I've proposed a potential fix at https://github.com/teorth/equational_theories/pull/1410 but I don't know for sure whether it is correct. That said, this one character fix cannot make things worse so maybe it should be urgently deployed, I don't know. EDIT: This worked out fine in the end.

[Bruno Le Floch]

@Terence Tao @Shreyas Srinivas Sorry to be a bother, but since many people will be looking at the Explorer, I figure I should ping you.

[Shreyas Srinivas]

Merged. It will still take CI one hour on the main branch. I didn’t review it.

[Shreyas Srinivas]

I doubt many people will be checking this out now. This project has been in the news a few times by this point and is a year old.

[Shreyas Srinivas]

In all fairness I am not in any of the relevant social networking sites.

[Bruno Le Floch]

Thanks a lot! Well, I think you underestimate Terry Tao's blog's readership.

FWIW the length of an array (containing the pieces after splitting at =) was compared to 2n (a BigNum) instead of 2. I checked my intuition that this was a problem with ChatGPT since I don't know Javascript.

The "I'm Feeling Lucky" button also does nothing I think, because we're done proving implications. Maybe someone with Javascript knowledge can look into it and propose something better like a message saying there no longer is any, or change the whole thing to any random implication instead of only unknown ones. But this is not at all urgent.

[Shreyas Srinivas]

That button was meant to randomly pick an unsolved implication as you suggest

[Shreyas Srinivas]

Also I just checked the blog. The post has only one comment

[Shreyas Srinivas]

Google search shows our preprint, the blogpost and one x (formerly twitter) post with very few likes and reposts in the last 24 hours

[Kevin Buzzard]

Me and many many many other people get a daily email from ArXiv (and have been doing so for decades) saying "here's all the number theory papers posted in the last 24 hours" and I suspect that many of us are reading those emails and clicking on papers -- it's part of my daily workflow. I'm sure the same will be true for whatever topic you chose for the equational theories paper. Forget what google says -- it landed in a whole bunch of people's inboxes very recently.

[Shreyas Srinivas]

There is basically zero chatter in ITP circles on mastodon and Bluesky

[Kevin Buzzard]

I think your view on how researchers behave is massively skewed towards how people your age behave. I essentially never look at social media at all.

[Shreyas Srinivas]

Okay that’s fair. All I am saying is this project has received quite a lot of attention already (talks at various venues, quanta articles etc).

[Bruno Le Floch]

Shreyas was partly answering my comment that Terry's blog post would have a significant effect bringing people to the Equation Explorer. I think your point about arXiv mailings is much more significant.

[Shreyas Srinivas]

So I wouldn’t expect too much academic interest. Those researchers who are curious about these things have probably already checked out the project by now.

[Shreyas Srinivas]

I am not saying there is no story to be written. The early days consisted of several sleepless nights of firefighting for me

[Douglas McNeil]

I look forward to the eight-part podcast "Gauls and other Problems: An Oral History of the Equational Theories Project". Move over, true crime, a new genre's in town.

[Shreyas Srinivas]

I actually have to collect my thoughts. First day I was feverishly experimenting with many dashboard tools from GitHub to trello

[Shreyas Srinivas]

And then I created a set of labels. Some of the label tasks could be managed inside GitHub’s GUI automation. I had to devise a systematic machinery for the rest.

[Shreyas Srinivas]

And then I put out a call for five CI tasks (it was either putting out a call or learning that smorgasbord of YAML and Bash overnight)

[Shreyas Srinivas]

Then Pietro stepped in and we have a long DM history of me explaining the precise tasks and him asking me questions and working his CI magic.

[Shreyas Srinivas]

And then Joachim joined as maintainer at some point to help with something very lean core specific

[Emmanuel Osalotioman Osazuwa]

Bruno Le Floch said:

Oops, the functionality to parse equations in the Equation Explorer is completely broken at present. I've proposed a potential fix at https://github.com/teorth/equational_theories/pull/1410 but I don't know for sure whether it is correct. That said, this one character fix cannot make things worse so maybe it should be urgently deployed, I don't know. EDIT: This worked out fine in the end.

This was my fault :smiling_face_with_tear: when updating the explorer to have infinite precision, I used vscode's built in find and replace features to update numbers like 0 -> 0n, 1 -> 1n, 2 -> 2n, ... which I had to manually roll back in some cases like the one above, but I must have missed this one. I missed it when testing the explorer, cause it was easier to type in a number than to type in the full equation string.
Thanks for spotting it, and getting it fixed.

[Alex Meiburg]

Since there's been discussion about promotion/discussion of the paper in other media, I would also like to let people know about SciRate: https://scirate.com/arxiv/2512.07087

It's particularly popular in the quantum information community (essentially just by chance and the self-reinforcing nature of such things; nothing about the website is geared toward QI); if anyone would so like, you can log in to give papers a "scite" to say something I like "I think this is interesting and worth highlighting".

[Shreyas Srinivas]

I don’t like the idea of highlighting my own paper as an author. It feels underhanded somehow. Giving a talk on invitation is a different matter.

[Alex Meiburg]

Sure, people have different feelings on this, and I also feel like it's very context-dependent. Just letting people know!