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.