Submitting the paper

Stream: Equational

[Terence Tao]

Thanks to everyone (and particularly @Shreyas Srinivas ) for the huge effort in getting the paper over the finish line and submitted to arXiv!

The next step is to work out where to submit the paper. We had two leading candidates, Annals of Formalized Mathematics and Journal of Automated Reasoning, but now would also be the time to discuss other potential options. I'm thinking of having an open discussion on this for a few days and then holding a poll for the coauthors at the end of it, but I will try to not bias the discussion with my own initial opinions and see if we can organically grow a consensus here.

[Shreyas Srinivas]

Since the topic has not received a response for a day, I wanted to remind everyone we already had a poll on this subject a while back

[Shreyas Srinivas]

And there was a lot of discussion on the factors that might affect the decision

[Shreyas Srinivas]

That discussion might give some useful perspectives for discussion here.

[Terence Tao]

Would you be willing to summarize that discussion here? I did see a remark from Kevin concerning diamond open access but I'm sure there were more considerations than that.

[Shreyas Srinivas]

I’m a bit tied up but this is roughly where the discussion began

https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Writing.20the.20paper/near/533228561

[Matthew Bolan]

Kevin's comment and some more discussion surrounding it is at #Equational > Writing the paper @ 💬 . I personally agree with Jose's thoughts here: #Equational > Writing the paper @ 💬 .

[Jose Brox]

For convenience, I am repeating those thoughts here:

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]

I have also asked his opinion to Fernando Vaquerizo Villar (who is not in Zulip). He doesn't think he is the right person to give an opinion about this, but his two cents are: even though he comes from CS, he would rather go with the risk of a new journal in Math than with a Q4 journal in CS, since that, for us junior postdocs at Spain, would be almost like throwing the paper away. But if instead there is the possibility of some suitable Q1 journal, that would be his preferred option (he has no potential journal to propose).

[Shreyas Srinivas]

I agree with Jose for the following reason: JAR is geared towards a CS audience that is not typically concerned with doing collaborative pure math at scale.

[Shreyas Srinivas]

It’s a niche within CS where people already know about working with ATPs. I can’t imagine that the collaborative aspect of working on math problems is interesting to them. We want mathematicians to read this paper since they have something new to learn from it.

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

We want mathematicians to read this paper since they have something new to learn from it.

Personally, I doubt that journal choice will shift the composition of the audience in any real way. Exaggerating a bit, it will change the identity of only 3 readers: the editor and the referees.

Everyone else will learn about the work through arXiv, word of mouth, literature search tools like Google Scholar, and citations in other articles. Those who don't have the inclination to read our paper will not change their mind based on which journal it appears in.

[Terence Tao]

/poll Which journal should we submit to? (co-authors only please)
Annals of Formalized Mathematics
Journal of Automated Reasoning

[Terence Tao]

I think we have enough discussion to open a poll. Co-authors, feel free to vote for both options, or to add additional options. I'll refrain from voting until the end to avoid biasing the process.

[Terence Tao]

We seem to be trending towards a decision, but I would like to have a quorum of the co-authors (which I will arbitrarily define as at least 50%, or 17) weigh in before settling the issue. Co-authors, please cast a vote if you haven't done so already!

[Mario Carneiro]

No one actually pinged the coauthors for this poll, so I'll take the opportunity to do so:
@Matthew Bolan @Joachim Breitner @Jose Brox @Nicholas Carlini @Mario Carneiro @Floris van Doorn @Andrés Goens @Aaron Hill @Hernan Ibarra @Zoltan A. Kocsis (Z.A.K.) @Bruno Le Floch @Amir Livne Bar-on @Lorenzo Luccioli @Douglas McNeil @Alex Meiburg @Pietro Monticone @Pace Nielsen @Giovanni Paolini @Marco Petracci @Bernhard Reinke @David Renshaw @Marcus Rossel @Cody Roux @Jérémy Scanvic @Shreyas Srinivas @Anand Rao Tadipatri @Terence Tao @Vlad Tsyrklevich @Daniel Weber @Fan Zheng @Harald Husum @Emmanuel Osalotioman Osazuwa

[Jose Brox]

Perhaps we should also consider Foundations of Computational Mathematics, which is a strong and well-respected journal too. What do you think?

[Terence Tao]

Given the outcome of the vote so far, I think we have enough of a (weak) consensus for Annals of Formalized Mathematics that I will go ahead and submit to that journal now. However, in the (hopefully unlikely) case that AFM rejects our paper, we can reopen this discussion with FoCM, JAR, and any other proposed journal as potential alternate venus.

[Bruno Le Floch]

Sorry, can you wait till the end of the weekend? I was chasing down some description of the E854⊨(finite)E10. I have a PR in progress.

[Terence Tao]

OK, I will wait for your PR.

[Jose Brox]

I have to add a couple of small things too (e.g. a forgotten acknowledgement).

[Jose Brox]

My PR is ready to merge! Mainly, I have redone one of the max_weight figures to remove some anomalous spikes coming not from Prover9, but from my OS.

[Jose Brox]

(Also, when I compile the pdf in my computer, I get an undefined control sequence error; I can override it, could be something related to my configuration, but could also be a real problem. The error message is the following: "! Undefined control sequence. \__hook begindocument/before ...IfPackageLoadedTF [...] {color}{}{\IfPackageLoaded... ")

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

I didn't have much time to look at the project in the last 6 months, so I didn't notice that the author list omits my middle inital, which I use in all my other academic work. I just submitted a PR that fixes this in the author list and metadata, but it already made it to the arXiv.

[Bruno Le Floch]

My PR is ready (CI finished). Three things still seem worth fixing at some point, but not by me.

• The introduction does not even try to announce how the paper is organized. Currently it only announces a few of the sections. In particular it's not clear to the reader what's going to happen in sections 2, 3, 4, 8, 11, 12, 13 and why they are split in this way.
• We mix \subsubsection and \textbf to split subsections into headings in section 7
• The arrow from "Claimed Task" to "Contributor disclaims a task" is annoyingly jagged

[Shreyas Srinivas]

I drew that figure in Libreoffice draw.

[Terence Tao]

I aligned the section 7 subsubsections. Not sure what useful thing to say about the paper organization though; the sections are largely independent of each other, and the section headings are reasonably descriptive already, so I'm not sure how to add more guidance beyond what the table of contents (and the existing section announcements) already state.

[Shreyas Srinivas]

Maybe we could briefly explain what’s in the blueprint vs what’s in the paper.

[Bruno Le Floch]

At some point it could be useful to detail a bit (in the blueprint?) what parts of the code are responsible for checking that all the implications have indeed been formalized. A referee could be interested.

[Terence Tao]

I've added a brief paragraph at the end of the introduction to the paper directing the reader to the blueprint for detailed descriptions of various components of the paper.

A summary of the full verification process would indeed be interesting, though I am not the best qualified to try to summarize it. I think a new blueprint chapter would be a reasonable venue for this. I don't think it needs to hold up the paper submission though, so if I don't hear any objections by the end of today, I'll go ahead and submit the current version to AoFM.

[Shreyas Srinivas]

I’m okay with submitting the paper as it is.

[Jose Brox]

Since AoFM explicitly says that
"Authors are required to first deposit their manuscript in an open archive: AFM accepts submissions from HAL, arXiv and Zenodo."
shouldn't we upload v2 to arXiv first, then submit to AoFM?

[Shreyas Srinivas]

This is easily done.

[Shreyas Srinivas]

What does it say about the repository itself?

[Shreyas Srinivas]

Do we actually have detailed setup instructions already?

[Jose Brox]

https://afm.episciences.org/page/instructions-for-authors

[Shreyas Srinivas]

I know people can set up the lean part. But what about all the CI based stuff?

[Shreyas Srinivas]

I submitted our repository for an SWHID. The status is "running"

[Shreyas Srinivas]

https://archive.softwareheritage.org/save/list/

[Terence Tao]

@Shreyas Srinivas will you be able to handle the arXiv update? I can submit after that update has gone through.

[Shreyas Srinivas]

Yeah I can do that

[Shreyas Srinivas]

Thanks to CI and arxiv’s new submission process, things ought to be much smoother

[Shreyas Srinivas]

We have an "undefined citation" problem
CC : @Terence Tao, @Jose Brox , and @Bruno Le Floch because your PRs are the most recent ones afaik

[Shreyas Srinivas]

Logged in as Shreyas_Srinivas_94 | Help | My Account | Logout
Start   >>   Add Files   >>   Review Files   >>   Process   >>   Metadata   >>   Preview

Submission Processing

Reprocess

There was a problem compiling your source. Please refer to log for details.
arXiv's automated TeX processing has failed to process your source. The 5 most common mistakes causing this are:

1. Mixed figure file formats. If you are using PDFLaTeX then all figures must be .pdf, .jpg, or .png formats. If your document uses (La)TeX all figures must be .ps or .eps. arXiv does not perform figure file conversion for you, please ensure your files are converted to the appropriate format before uploading.
2. Default hyperref failures ("Option clash for package hyperref") are not a reason to report a failure to arXiv. Continue scrolling in the log to find the specific errors that are being flagged.
3. Missing customized or differing version of style files.
4. Missing, misnamed, or local complete paths to figure files. arXiv's file system is case sensitive.

To upload or edit your files before reprocessing return to the add files step.

The TeX Log appears below.
Need help?
You may wish to hit "Ctrl + F" ("Command + F" on a Mac) to search for "error" on this page.
If you are unsure of what your specific failure is please review our help pages, knowledge base or searching the internet for your specific processing messages.
Or contact us citing submit/7063426. We will work with authors to help resolve TeX processing issues and if we determine that there is not a ready solution we will consider allowing PDF instead of TeX. We try to provide same day replies for submission help Monday-Friday.

Compilation Summary

Our system failed to process your submission using pdflatex. Status: [FAILED]


Files that were processed as part of this submission:

main.tex => main.pdf [FAILED]
...at step "second_run:0"
...reason for failure: "compiler run returned error code"


Our system failed to generate a PDF.

Selected Errors and Warnings

Your paper has a problem which you need to fix before it can be accepted by arXiv.

    One or more citations are undefined. Please ensure all citation keys are present in your reference list.



Errors for main.tex:

    Undefined citation (75 total)
        A referenced citation is undefined.
        LaTeX Warning: Citation `Tao_blog_Sep_2024' on page 1 undefined on input line 3.
        Please ensure all cited references are defined and that all citation keys are present in your reference list.
        A referenced citation is undefined.
        LaTeX Warning: Citation `term-rewriting' on page 2 undefined on input line 11.
        Please ensure all cited references are defined and that all citation keys are present in your reference list.
        A referenced citation is undefined.
        LaTeX Warning: Citation `mccune-survey' on page 2 undefined on input line 11.
        Please ensure all cited references are defined and that all citation keys are present in your reference list.
        ...

    Lower level TeX Errors (5 total)
        Package minted Error: Missing definition for highlighting style "default" (minted executable is unavailable or disabled); attempting to substitute fallback style..
        ./foundations.tex:59: Package minted Error: Missing definition for highlighting style "default" (minted executable is unavailable or disabled); attempting to substitute fallback style.
        Please refer to details in the log.

        Package minted Error: Cannot highlight code (minted executable is unavailable or disabled); attempting to typeset without highlighting..
        ./foundations.tex:59: Package minted Error: Cannot highlight code (minted executable is unavailable or disabled); attempting to typeset without highlighting.
        Please refer to details in the log.

        Package minted Error: Cannot highlight code (minted executable is unavailable or disabled); attempting to typeset without highlighting..
        ./foundations.tex:77: Package minted Error: Cannot highlight code (minted executable is unavailable or disabled); attempting to typeset without highlighting.
        Please refer to details in the log.

[Shreyas Srinivas]

The citation undefined error usually indicates a more serious error. Especially if all citations are failing

[Jose Brox]

I already mentioned that when I downloaded the paper and compiled it locally, I got the following error in WinEdt:
"! Undefined control sequence. \__hook begindocument/before ...IfPackageLoadedTF [...] {color}{}{\IfPackageLoaded... "
This doesn't seem related to my changes, which were minimal.

[Shreyas Srinivas]

locally I find that the error is at the point where minted is declared

[Shreyas Srinivas]

Did we use minted from the beginning?

[Jose Brox]

Seems since #1406 last week

[Shreyas Srinivas]

CC : @Marcus Rossel

It seems arxiv doesn't like minted

[Shreyas Srinivas]

I have never dealt with this minted before outside overleaf

[Jose Brox]

Solutions in here:
https://tex.stackexchange.com/questions/280590/work-around-for-minted-code-highlighting-in-arxiv
(See newest messages at the bottom, probably https://tex.stackexchange.com/a/725077/73874 will work)

[Shreyas Srinivas]

okay. I can try these tomorrow morning. But ideally this minted PR should not have been made/merged without a warning about this issue.

[Jose Brox]

Shreyas Srinivas ha dicho:

I submitted our repository for an SWHID. The status is "running"

How does this work? Is it dynamic, updated with the site, or is it a snapshot? If the latter, perhaps we should stop it until we completely fix the paper.

[Shreyas Srinivas]

We can resave it

[Shreyas Srinivas]

I can't make any sense of that fix because I tried the tex.stackexchange solution and I am getting complaints about shell-escaping latex. Can someone make a PR with the pygments cache files and the changes?

[Shreyas Srinivas]

maybe also include minted.sty locally

[Jose Brox]

From arXiv common mistakes/minted:

Notes for using minted.sty in arXiv

arXiv cannot process using the --shell-escape option, as this is disabled in arXiv's system for security reasons.

Authors who make use of minted.sty's syntax highlighting are warned against using so called "hidden" cache directories in arXiv. This means that if you are running with their recommended [frozencache] option to the package, you will need to specify a cache directory. Do not use a hidden directory name! Hidden directories begin with the special . character, such as .minted-cache (which may be the default). Such options will break at publish time, as these files are not saved between compilation and publication (and are not able to be regenerated). To account for this, do not use them. An example of a correct call looks like:

  \usepackage[frozencache=true,cachedir=minted-cache]{minted}

This assumes that you've already correctly created the cache first using their [finalizecache] option. Consult the package manual for further details (at time of this writing, the package options begin on page 12 in section 5).

[Shreyas Srinivas]

that's fair. But my local machine cannot compile this

[Shreyas Srinivas]

My latex setup is a bit old since i have been using overleaf for my ongoing papers (except this one)

[Shreyas Srinivas]

That is why I am asking someone to make the PR with the correct cache folder and cache files and the final latex config for importing minted

[Jose Brox]

Seems that minted v3 does not need (and does not use) the
[finalizecache] option. I'm not sure what should I do for that PR. Do I just include [frozencache=true,cachedir=minted-cache] for the minted package? And those cache files, *.pygtext and *.pygstyle, aren't produced after compilation? (I cannot compile the pdf locally yet, it still gives me the same error as before, seemingly unrelated to minted).

[Shreyas Srinivas]

I am really no help here since I am not even able to compile this. Hopefully someone with prior experience with minted can chime in

[Jose Brox]

Someone simply avoided minted and shifted to listings to mimick minted (with 2 colors):

\usepackage{listings}
\usepackage{xcolor}

% Define our colors
\definecolor{stringcolor}{RGB}{186,33,33} % Minted-like string color #BA2121

\lstdefinestyle{numberedlist} {
language=Python,
basicstyle=\ttfamily\small,
keepspaces=true,
columns=flexible,
numbers=left,
numberstyle=\tiny\color{gray},
numbersep=5pt,
stepnumber=1,
% String handling
stringstyle=\color{stringcolor},
showstringspaces=false,
% Escape to LaTeX
escapeinside={@}{@},
}

\lstset {
language=Python,
basicstyle=\ttfamily\normalsize,
keepspaces=true,
columns=flexible,
% String handling
stringstyle=\color{stringcolor},
showstringspaces=false,
% Escape to LaTeX
escapeinside={@}{@},
}

\lstdefinestyle{smallsize} {
language=Python,
basicstyle=\ttfamily\small,
keepspaces=true,
columns=flexible,
% String handling
stringstyle=\color{stringcolor},
showstringspaces=false,
% Escape to LaTeX
escapeinside={@}{@},
}

[Jose Brox]

Hey, the arXiv note on common mistakes is outdated. They have a newer note on their Tex Live page, which says something simpler:

Note in particular that minted got a completely new version in TeX Live 2025, and the previous behavior and arguments to the \usepackage[...]{minted} call need revision. Most recipes given on the internet are still referring to minted version 2 or below, while TeX Live 2025 uses minted version 3.

As a simple recipe:

• Use \usepackage{minted} in your document, and run (pdf)latex once with -shell-escape. This should create a directory _minted.
• Include the _minted directory in your upload. No further changes are necessary. In particular, using options like frozencache etc are now unnecessary.

You can check success by running (pdf)latex -no-shell-escape and check whether errors related to minted occur.

[Shreyas Srinivas]

I think this works provided you can locally compile the latex and produce the minted directory

[Jose Brox]

(I can't compile locally because of my extra error). Related: Idk how the pdf is actually compiled from github.com to github.io. Can't you locate the output files somewhere?

[Jose Brox]

I had to update my outdated MikTeX install to get rid of some errors. I have now been able to compile the paper with the -shell-escape option, then it recompiles with the -no-shell-escape option, so it worked. But it didn't create a _minted directory, but a _NAME.data.minted file. @Shreyas Srinivas can you check if it works for you on arXiv?

_FAD58DE7366495DB4650CFEFAC2FCD61.data.minted

[Jose Brox]

(According to ChatGPT, the _minted directory is a feature of older versions of minted, which v3 changed to a file)

[Jose Brox]

Unrelated: I have detected misalignments in Table 1 (column 2) and Table 4 (rows 16-19). I have asked @Bruno Le Floch if those are intentional.

[Shreyas Srinivas]

Okay but please PR this. I’m not on a machine for another 10-12 hours

[Jose Brox]

From what I gather from arXiv's instructions and ChatGPT, we just need to include the _NAME.data.minted file in our arXiv upload (no line needs to be changed in the .tex file).

[Shreyas Srinivas]

Okay. I’ll just upload the folder

[Jose Brox]

Perhaps we should fix the Tables issue before submitting.

[Bruno Le Floch]

Table 4 is aligned at the decimal point, which allows comparison of numbers. I think this is standard? It looks slightly odd because the first few numbers have two digits after the decimal point, and then later numbers have no digits after the decimal point, but that's the data we have. We could drop the last digit in 38.82 I guess to make this clearer.

Table 1 might be bad, it doesn't look so nice indeed. But I'm not sure what alignment to prefer there. Happy to make a change and PR today if anything is suggested.

[Bruno Le Floch]

For reference, here are the tables in question:

https://leanprover.zulipchat.com/user_uploads/3121/MPDHDd5by8KmRnOUpTdZu-Gz/image.png

https://leanprover.zulipchat.com/user_uploads/3121/uYxlHkju_z0FPSpktjm848Ja/image.png

[Jose Brox]

Since my eyesight isn't normal, it is better if other people can comment on this.

[Jose Brox]

@Shreyas Srinivas about the
minted package issue: Ideally we'd want to have the problem solved even if we need to recompile the paper on CI (moreover, if we also compile locally in order to add the .minted file later, we should check that all minted highlights etc. are where they should be, what is cumbersome).

If I'm understanding correctly, on CI we are compiling through GitHub actions using YAML. I don't really know about this, but from what I gather, in order to get as output not just the pdf file, but also the minted file (whose name is some unknown hash), I think we should write something like

name: Upload PDF and minted data file
  uses: actions/upload-artifact@v4
  with:
    name: pdf-and-minted
    path: |
      main.pdf
      *.minted

Here I'm assuming the version of minted running via GitHub is v3, which will generate just one file instead of a folder (and in addition we don't need to add any extra options when including the minted package into the tex file). If GitHub uses an older version, then we may have problems, since arXiv seems to use v3.

[Marcus Rossel]

@Jose Brox @Shreyas Srinivas Sorry, I was not aware that there were problems with minted for Arxiv.

When I build the paper locally (with TeX Live 2025 and minted v3.6.0), I do get a _minted directory. Also, AI tells me that "Starting with minted v3.0.0 and later, the package by default creates a cache directory named _minted in your project directory when it runs." If it helps, I could just add the _minted directory to the repo for now. I'd have to look more into how to do this with CI - wouldn't know off the top of my head.

[Shreyas Srinivas]

Please do this

[Marcus Rossel]

@Shreyas Srinivas https://github.com/teorth/equational_theories/pull/1422

[Bruno Le Floch]

What about replacing the minted package by the listings package? The syntax highlighting is less clever (since it is done within TeX instead of externally), but it avoids needing to keep temporary files up to date. See https://github.com/teorth/equational_theories/pull/1423 if people choose this option. I'm fine either way.

[Shreyas Srinivas]

I tried submitting again. It didn't work. Same error

[Shreyas Srinivas]

I recommend not using minted. Minor formatting details are not worth this much effort.

[Shreyas Srinivas]

@Bruno Le Floch : I have merged your PR

[Shreyas Srinivas]

latex experts : what does entry type for "FLT_Lean" isn't style-file defined mean?

[Shreyas Srinivas]

Another issue :

./automated.tex:96: LaTeX Error: Invalid UTF-8 byte "87.

See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...message LaTeX Error: Invalid UTF-8 byte "\UTFviii@hexnumber {`\xc2\x87}.

[Shreyas Srinivas]

what changed there?

[Shreyas Srinivas]

There are a whole bunch of these unicode character errors now

[Shreyas Srinivas]

Examples:

[66]

[67]

[68]) (./contributions.tex
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x9c ("201C) in font ec-lmr12!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x9d ("201D) in font ec-lmr12!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x9c ("201C) in font ec-lmr12!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x9d ("201D) in font ec-lmr12!


[69]) (./main.bbl

[70]

[71]
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmr10!
Missing character: There is no \xc3\x85\xc2\xa1 ("161) in font ec-lmr10!

Underfull \hbox (badness 1314) in paragraph at lines 191--195
[]\T1/lmr/m/n/10 Andrzej Kisielewicz. Austin iden-ti-ties. \T1/lmr/m/it/10 Al-ge-bra Uni-ver-salis\T1/lmr/m/n/10 , 38(3):324--328, 1997. []$\T1/lmtt/m/n/10 doi : 10 . 1007 /
[]



[72]
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmri10!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmri10!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmr10!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmr10!
Missing character: There is no \xc3\xa2\xc2\x80\xc2\x93 ("2013) in font ec-lmr10!

[Shreyas Srinivas]

can someone else take over this v2 submission. I am no good with these latex errors, and tbh we had a perfectly functional latex submission and now somehow it's all messed up and I have no clue how to fix it.

[Shreyas Srinivas]

I am guessing since all of you own the preprint, this should be possible. Points to note:

1. out SWHID is : swh:1:snp:2b9a68ae6968502fac0166990e19be9b05ef0d0d;origin=https://github.com/teorth/equational_theories
2. Zoltan's name on the metadata page should be changed to "Zoltan A. Kocsis". It currently doesn't have his middle name initial "A"

[Bruno Le Floch]

entry type for "FLT_Lean" isn't style-file defined can be ignored in our case: it means that the BibTeX style we use (plainurl) does not know what to do with @software and a few other kinds of entries in our bibliography file references.bib. And that means BibTeX treats them as @misc, which is fine.

[Shreyas Srinivas]

@Bruno Le Floch has the token for the arxiv submission

[Bruno Le Floch]

I've had to do some minor changes, CI just started running on my PR https://github.com/teorth/equational_theories/pull/1424 and I want to make sure that everything goes well and the PR is merged before going forward with submission. Given how late it's getting here, I'll submit tomorrow during lunch break.

[Shreyas Srinivas]

Thanks a lot for carrying this through

[Shreyas Srinivas]

Oh wait you actually made a better lstlistings config. Thanks even more.

[Bruno Le Floch]

It is very incomplete since it only has the keywords that appear in our specific code listings. On the other hand I was quite happy to get the correct highlighting of «Facts from All4x4Tables [[1,2,3,4,5,0],[4,1,2,5,0,3],[3,0,5,2,1,4], [0,5,4,3,2,1],[5,4,1,0,3,2],[2,3,0,1,4,5]]».

[Bruno Le Floch]

@Shreyas Srinivas I plan to submit (the appropriate files in the paper/ directory in) the current latest commit to the arXiv. Can you easily regenerate the SWHID? Otherwise I'll do this over lunch.

[Shreyas Srinivas]

I have requested a “save again”

[Shreyas Srinivas]

You can find our archive here: https://archive.softwareheritage.org/browse/origin/directory/?origin_url=https://github.com/teorth/equational_theories&timestamp=2025-12-16T09:58:01Z

[Shreyas Srinivas]

Here is the swhid

swh:1:dir:426b52ba40033a37c18474ef44068e23c55df4bc;origin=https://github.com/teorth/equational_theories;visit=swh:1:snp:7954c0d5160b32085577accc3ac6ba2ca3169cf5;anchor=swh:1:rev:14cf5e235384d0aea262b8580892a783100b3daf

[Shreyas Srinivas]

I will also push a tag

[Shreyas Srinivas]

@Bruno Le Floch please also change Zoltan’s name to include his middle initial.

[Bruno Le Floch]

Is it ok if I use only the "core" part of the id, namely swh:1:dir:426b52ba40033a37c18474ef44068e23c55df4bc, which identifies uniquely the software artifact, namely the actual contents of the files, but does not include the information that it was hosted at github and other metadata? Putting the whole qualified SWHID in the arXiv comment field looks horrendous.

[Shreyas Srinivas]

Sure

[Shreyas Srinivas]

We can also link to the GitHub repo separately

[Shreyas Srinivas]

In the comment field.

[Bruno Le Floch]

I'll point to the home page https://teorth.github.io/equational_theories/ instead of the repo.

[Bruno Le Floch]

Article submitted, with Zoltan's middle initial, Fan Zheng's last letter, comment field containing a link to the home page and the core SWHID. Preview pdf file: ETP-arxiv-v2-preview.pdf.

email from e-prints@arxiv.org

We have received your replacement of 2512.07087. Your temporary
submission identifier is: submit/7085268.

You may update your replacement at: https://arxiv.org/submit/7085268

Your replacement is scheduled to be announced at Wed, 17 Dec 2025 01:00:00 GMT.
The abstract will appear in the subsequent mailing as displayed below,
except that the submission identifier will be replaced by
the official arXiv identifier. Updates before Tue, 16 Dec 2025 19:00:00 GMT will
not delay announcement.

If you have a problem that you are not able to resolve through the web
interface, contact [help@arxiv.org](mailto:help@arxiv.org) with a description of the issue and
reference the submission identifier.

arXiv admin
------------------------------------------------------------------------------
\\
[arXiv:submit/7085268](arxiv:submit/7085268)
From: Bruno Le Floch [<bruno@le-floch.fr>](mailto:bruno@le-floch.fr)
Date: Mon, 8 Dec 2025 01:43:56 GMT   (3661kb)
Date (revised v2): Tue, 16 Dec 2025 09:29:54 EST   (3345kb,A)

Title: The Equational Theories Project: Advancing Collaborative Mathematical
  Research at Scale
Authors: Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario
  Carneiro, Floris van Doorn, Martin Dvorak, Andr\'es Goens, Aaron Hill, Harald
  Husum, Hern\'an Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne
  Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone,
  Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco
  Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux,
  J\'er\'emy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad
  Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng
Categories: math.RA cs.LO
Comments: 74 pages; https://teorth.github.io/equational_theories/
  swh:1:dir:426b52ba40033a37c18474ef44068e23c55df4bc
License: http://creativecommons.org/licenses/by/4.0/
\\
  We report on the Equational Theories Project (ETP), an online collaborative
pilot project to explore new ways to collaborate in mathematics with machine
assistance. The project successfully determined all 22 028 942 edges of the
implication graph between the 4694 simplest equational laws on magmas, by a
combination of human-generated and automated proofs, all validated by the
formal proof assistant language Lean. As a result of this project, several new
constructions of magmas satisfying specific laws were discovered, and several
auxiliary questions were also addressed, such as the effect of restricting
attention to finite magmas.
\\

• Files that are not used to produce the pdf should go in an anc/ directory, so I put contributions.md there for the arXiv submission.
• Instead of references.bib I put the generated main.bbl as otherwise the HTML conversion was failing to produce a bibliography.
• I've reported two other issues to the arXiv about the HTML conversion.

[Bruno Le Floch]

v2 is live. @Terence Tao It's now technically possible for you to submit to the journal. I'll let you decide at which stage you want to seek the formal agreement of all authors.

[Terence Tao]

At this point I think everyone except for @Fan Zheng has weighed in; I will make one final effort to contact him today, but he did at least consent to being a co-author and supplying his contributions in the past via Zulip discussion (see #Equational > Drafting the paper @ 💬 ).

[Vlad Tsyrklevich]

I will share one possible email for them over DM.

[Terence Tao]

I have now submitted the paper to Annals of Foundational Mathematics. (The arXiv overlay made this procedure painless from my end, though of course Bruno and Shreyas had to do a lot more technical heavy lifting to make the arXiv submission possible!)

One issue that came to mind during the submission process. Up until now we have used this open channel to coordinate the project. However, it may make sense for discussion of the publication of the paper (and any referee reports we recieve, etc.) to move to a private channel (or group DM, email chain, etc.) involving only the co-authors of the paper. I am not sure how to proceed on this, and would like to open a discussion regarding this (and perhaps follow up with a poll, as with previous questions of this nature). Anyway, would welcome opinions both from co-authors and from interested observers on this point.

[Shreyas Srinivas]

We can ask the Zulip moderators to make a private channel for this.

[Kevin Buzzard]

I've seen several instances of a private channel created when people are working on a project but this is the first time I've seen a request for a private channel for a project after it is finished! I can certainly make one but ideally you would have a moderator or someone trusted by the community to make sure that there is no inappropriate behaviour. Probably @Pietro Monticone would fit the bill -- Pietro would you be wiling to keep an eye on the channel? If so I can create it (assuming someone else didn't do this already). My instinct usually in this situation would be to just tell you to retreat to DMs but because so many people were involved I can see the logic in a private channel, DMs will be unwieldy.

I would need to know a name for the channel and a "brief description" (e.g. the brief description for this channel, Equational, is "Coordination for the Equational Project"). The brief description can be changed but I think it's more of a pain to rename the channel itself.

[Pietro Monticone]

Thank you, @Kevin Buzzard. Sure, feel free to add me as the private channel moderator.

Here is a proposal:

• Channel Name: "ETP Paper"
• Description: "Private channel for co-authors to discuss submission status, referee reports, and revisions for the Equational Theories Project paper."

[Kevin Buzzard]

OK Pietro, Shreyas and Terry should be subscribed and hopefully you guys can take it from there.

[Pietro Monticone]

Thank you!