Drafting the paper

Stream: Equational

[Terence Tao]

Now that we have (provisionally) resolved all implications in the main implication graph, we can now turn to the process of writing the paper associated to the project. Building on some earlier work of @Pietro Monticone , the plan of the paper has now been converted to a LaTeX document (PDF here), which is broken up into multiple files in https://github.com/teorth/equational_theories/tree/main/paper that can be worked on separately.

In an old discussion, we had tentatively settled on having a large number of authors of the paper, ordered alphabetically, and in an appendix listing the author contact information, affiliations, and contributions, using the standard CReDiT system categories as a template. It is perhaps good to continue discussion in this; it was pointed out that the categories do not perfectly align with the roles we have ended up assigning here, and we may want to add re-interpretations of the categories as needed. In the meantime, I have made a mockup in the paper of how I imagine the author listing would go, using myself as an example. My thought was to have all contributors who wish to be listed as an author self-report their contributions in this fashion via PRs, but am open to discussion on this process. [EDIT: to perhaps forestall potential spam or other frivolous attempts to subvert the process, the PR should be accompanied by a more detailed self-description of the contributions to the project for the moderators to approve.]

Anyway, I would like to discuss next steps. Perhaps we can discuss section structure, and if some sections are stable enough in intended content, we can create issues on Github for individuals to work on expanding them.

[Shreyas Srinivas]

For the project management section I would like to prepare a free flow draft before planning and structuring it better

[Terence Tao]

OK. Should we create a formal issue for this to "reserve" project.tex for now so that no-one else edits it in the meantime?

[Shreyas Srinivas]

Yes

[Terence Tao]

opened equational#873.

[Shreyas Srinivas]

We can create a column in the project dashboard to of author contribution issues. I'd suggest a one or two sentence description of your contributions to the project, using suitable conjunctions and clauses such as :

1. "I built the XYZ tool"
2. "I developed (and/or) formalised abc approach to prove/refute such and such class of implications", or, "I authored XYZ in the blueprint/paper"
3. "I mentored XYZ to do ABC"
4. "I maintained such and such aspects/tools"

Sometimes your contributions could be much more scattered. You might have participated in the discussion of some refutations, and in that, you might have found a variation of an idea or run an ATP on some constraints or even found a bug. I suggest that summarising them all in a sentence and maybe using GitHub comments to add details.

[Terence Tao]

We could do this, but to me this seems roughly equivalent to asking everyone to submit a PR to directly adjust contributions.tex in which they can describe their contributions in Github comments. Are there any particular advantages to routing it through the Github projects page?

[Bruno Le Floch]

It would be useful to have guidance on how much participation is required for authorship (in particular if moderators have to decide, it is best if they can do so consistently).

A related question is the scope of the article, as the main project gave a few off-shoots that are not all closely tied to it (the study of order 5 equations, Higman-Neumann axioms, the finite implication table).

[Shreyas Srinivas]

Terence Tao said:

We could do this, but to me this seems roughly equivalent to asking everyone to submit a PR to directly adjust contributions.tex in which they can describe their contributions in Github comments. Are there any particular advantages to routing it through the Github projects page?

I don't mind it that way either. It's just that depending on how we merge the PRs, other PRs will have to constantly fix merge conflicts

[Shreyas Srinivas]

Because all 45 PRs are touching the same file

[Shreyas Srinivas]

Bruno Le Floch said:

It would be useful to have guidance on how much participation is required for authorship (in particular if moderators have to decide, it is best if they can do so consistently).

A related question is the scope of the article, as the main project gave a few off-shoots that are not all closely tied to it (the study of order 5 equations, Higman-Neumann axioms, the finite implication table).

As a computer science person, I have a broad understanding of the term contribution. Keeping in mind the unconventional nature and form of this project, contributions can range from good theoretical ideas, to formalisation, blueprint write ups, maintenance work, authorship, mentorship on some portion of the project, etc. On the technical side you might have added some proof, or improved and fixed another person's proof, fixed bugs in the proof search prcedures, or even simplified an existing refutation for formalisation purposes. On the other hand I don't know how far it should go. This contribution elicitation process should allow a good filter. If someone feels they didn't contribute much, they might hesitate to add their names since it will appear along side their contribution.

[Pietro Monticone]

I tend to prefer to approach this systematically by discussing, interpreting, and extending each of the CReDiT categories.

Once these extended categories are well-defined and agreed upon, individual contributors can easily identify their contributions across the relevant categories and propose to attribute them accordingly via a PR filling a simple table with :check:.

We could have a longer, less schematic description too written below the table to make sure that some major not-easily-classifiable contribution is not left out.

[Fan Zheng]

@Terence Tao Should we have an array of tools to generate models of a given equation in the paper?

[Terence Tao]

Yes, I plan to make such a list in the introduction soon, and then create some sections in the paper to discuss individual techniques (or families of techniques).

[Pietro Monticone]

Here is the temporary markdown file containing the contributions table mentioned above with the default (i.e. not yet interpreted and extended) categories: https://github.com/teorth/equational_theories/blob/main/paper/contributions.md.

[Terence Tao]

I like this table approach. At equational#844 I made a sample PR in which I add my name and appropriate checkmarks to the table, and explain in the PR my justification for the categories. Hopefully this is a suitable workflow for everyone else to add to the table as well? The one issue is with merge conflicts. I was thinking of perhaps first collecting a list of contributors, adding them as rows to the table, and then allowing PRs for each person fill in their row; hopefully this will allow git to work out how to avoid conflicts.

I interpreted "Investigation" as "worked to analyze at least one implication", and "Methodology" as "developed at least one technique to analyze implications". Some categories may end up being unused; we had no funding and I don't think there was any supervision/mentoring happening, but perhaps there was some activity of this sort that I was unaware of.

[Terence Tao]

One activity which does not seem well represented in current categories is contributing to the blueprint for the project. Perhaps either "Data Curation" or an extended category?

[Terence Tao]

/poll Are you interested in being a co-author in the report for this project?
Yes. I have made at least one contribution to the project, and will submit a PR describing my contributions in due course.
No, but I would be happy to be listed as a participant in the acknowledgments section.
No, I do not wish to be either a co-author or listed as a participant.

[Terence Tao]

I guess there may be some co-authors who do not use Github. We can discuss (either in this thread, or by private DM) if there should be an alternate way to declare one's contributions that does not involve a Github PR, if this is an issue.

[Terence Tao]

For now, if there is a co-author or acknowledgment request that one would prefer to submit privately, you can DM me and I can try to work out some reasonable solution.

[Pietro Monticone]

Maybe all the code review, code cleaning and upstreaming should go under “Software”?

[Terence Tao]

Either that or "Data Curation". It's possible that some contributions span more than one category.

[Pietro Monticone]

What about CI infrastructure design and development?

[Terence Tao]

Hmm, that could plausibly go under "Software" or "Validation", I think. Maybe "Validation", though I was thinking of using this category for Lean formalization, so maybe we would split into subcategories if we want to make the distinction. (Or we could just keep the CReDiT categories as they are for the paper, and rely on the individual PR self-descriptions for any nuances.)

[Terence Tao]

I created a contribution label for PRs, so that we can go find all the contributions of all the coauthors later if need be.

[Terence Tao]

Regarding co-authors that don't use Github: I guess I can just submit a PR on behalf of anyone who doesn't want to use Github directly. I titled my own PR with my own name, but I could just as easily submit PRs for other people by mentioning their name in the title.

[Pietro Monticone]

I think it might be good if, for each category, contributors could add a link to a representative contribution (specific commit, PR, Zulip topic, others).

[Terence Tao]

Good idea, I will update my own PR to do this later today. [UPDATE: now done.]

[Pietro Monticone]

Just to facilitate reviewers’ work

[Terence Tao]

Regarding the blueprint, we could declare it to be "metadata", in which case all blueprint contributions would come under "Data Curation". (It's a bit of a stretch, but the categories will likely just be a zeroth order approximation no matter what, and I'm leaning towards using the PR descriptions as the more definitive reference for precise contributions.)

[Shreyas Srinivas]

What category does helping fix formalisations fall in? I think we could have a category that is or subsumes "maintenance"

[Terence Tao]

Hmm. None of the categories are a great fit, but "Data Curation" or "Validation" could work I think.

[Terence Tao]

I've gone ahead and added rows to contributions.md for everyone so far who has identified as a co-author. If there are no objections, I think it is now fine for people to PR their contributions modifying each row (I'm hoping this does not create merge conflicts) and provide some brief justification of each entry with some representative links (like I did at https://github.com/teorth/equational_theories/pull/884 as a template). If the PRs have the title "Contributions - <name>" and use the contribution label then it should be easy to organize them for future reference.

I estimate it will take at least a month to get the paper finalized (and of course we still have 50 odd statements to formalize), so there is absolutely no rush on this.

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

Helping with formalizations seems to fit well under Validation.

I think we could have a category that is or subsumes "maintenance"

It's tempting to create more and more precise categories, but I'm not sure it'd be all that useful in the long run. CReDiT seems to be a well-designed standard for describing the different types of contributions people made, and communicate them reasonably clearly to the referees, readers and even to onlookers.

Should historians, hiring panels, tenure committees or anyone else ever need a more in-depth account of specific contributions made by specific individuals, they’ll still have (and will want to use) the Github repositories and Zulip discussions as primary sources, assuming no catastrophic data loss occurs.

[Terence Tao]

My inclination is to try using the standard CReDiT categories first and see whether they are a reasonable fit. If we keep having lots of square-peg-in-round-hole issues then we can always refactor later.

[Terence Tao]

@Pietro Monticone has just completed his contributions PR at equational#891. This can serve as a template for other such PRs.

[Fan Zheng]

@Terence Tao I'm not using Github so I'll declare here. So far my contribution is the proof that equation 477 is confluent, as is also shown latter by some automated tools. I'm not sure what category that falls in. Also is there any interest in listing all known confluent (maybe after completion) equations? Or more generally, all equations with a "universal model" in which its implication to other equations can be checked directly? If there is, then I have some work done already and you can start from equation with 3 operations.

[Terence Tao]

@Fan Zheng I've marked you down at equational#896 for "Investigation" and "Methodology". You are also welcome to contribute to "Writing", for instance if you want to share your work on equations with a known universal model (there are currently stubs in the paper for "Confluence" and "Complete rewriting systems" that may need some volunteers to help write, as this is not a topic I am expert in).

I think @Amir Livne Bar-on had some listing of confluent and/or confluent-after-completion equations, but I don't know how exhaustive this list is.

[Matthew Bolan]

I'd like to help write the paper/blueprint if there is a section appropriate for me. Perhaps if the formalizers desire it I can write up some of the remaining vanilla greedy algorithms in detail.

[Terence Tao]

That would be helpful actually! I just PR'ed some additions to Section 7.4 of the blueprint that should land soon that put in some of the text from the various outstanding greedy arguments (expanding upon the previous version that just discussed 1722), but perhaps there is a way to organize the material in a more coherent way that reduces repetition and may suggest a more systematic way to formalize. If you'd like to take a stab at organizing that blueprint material, that could be helpful (and also give some insight as to how to arrange the corresponding section of the paper, currently a stub at Section 5.5).

[Terence Tao]

created equational#902 to officially record this (so that the rest of us know that this section is being worked on).

[Matthew Bolan]

Alright, I couldn't work on it as much as I would have liked to today, but I made equational#912 which adds the remaining algorithms to the blueprint. I also of course corrected 1722 and added some detail about its square case.

[Matthew Bolan]

There still are some easy arguments handwaved away, but I think the situation should be better than it was this morning. I can continue to work on this if it seems important. Besides 1722, 63 proved tricky for me to understand, so I added some detail there about how Law 2 is used to avoid various edge cases.

[Terence Tao]

Thanks! Hopefully this is a sufficient level of detail to help with formalization. I'll update the issues to point to the blueprint once it lands.

[Terence Tao]

Opened some issues equational#920 equational#921 equational#922 equational#923 equational#924 to write first drafts of specific sections of the paper. There are some sections that I'm leaving fluid for now, such as the conclusions section, but this should already get us a long way to a reasonably complete first draft.

[Andrés Goens]

One thing I'm not sure about here is the target audience, should the paper have an audience that's about as general as the group of contributors (e.g. shhould we assume no background in any specialized subfield like, just a general ineterest in this intersection), or are we targeting a particular, albeit wide, audience (e.g. mathematicians at large, computer scientists), etc?

[Daniel Weber]

What background knowledge could be relevant? There's some logic, what else?

[Amir Livne Bar-on]

Fan Zheng said:

Terence Tao I'm not using Github so I'll declare here. So far my contribution is the proof that equation 477 is confluent, as is also shown latter by some automated tools. I'm not sure what category that falls in. Also is there any interest in listing all known confluent (maybe after completion) equations? Or more generally, all equations with a "universal model" in which its implication to other equations can be checked directly? If there is, then I have some work done already and you can start from equation with 3 operations.

There is a listing of equations that are confluent as one-rule rewriting systems. This was generated by the script in the same directory. The script can only detect equations whose LHS is x, and not equations that have operations on both sides. I wrote this script from scratch after some armchair-thinking about the problem, and improved its algorithms when new classes of confluent equations were found. I later understood from Cody Roux's explanations on other threads that the final method is complete for this class of equations. The code and the data may still have some bugs: the full output wasn't verified by any other automatic method (either Lean or existing implementations of rewriting systems).

In addition to equations that are confluent as a 1-rule rewriting system, there are some that are solvable by the Knuth-Bendix algorithm, meaning that they become confluent after adding more rewriting rules. These aren't included at all.

[Jose Brox]

Terence Tao ha dicho:

Opened some issues equational#920 equational#921 equational#922 equational#923 equational#924

I'm new to Github and there are things that I don't know yet. Can an issue be claimed by several people at the same time? Writing paper sections can be very collaborative. I'd be glad to claim the Higman-Neumann section, but it would benefit if @Bruno Le Floch and @Vlad Tsyrklevich can also collaborate at the same time (if they want/can).

[Vlad Tsyrklevich]

Just to be clear: the ability to 'claim' an issue is specific infrastructure for this project, not GitHub generally. The way it works is that only a single person can claim an issue, but you can think of this as a formality to avoid unwitting duplication of effort. There's nothing to stop you from working with others.

[Andrés Goens]

Daniel Weber said:

What background knowledge could be relevant? There's some logic, what else?

well, most of the refutations use some basic constructions that require some undergradute level of algebra/analysis at least, many potential readers with a computer science or AI background wouldn't know that. Or for for example in the context of ATPs, it makes sense to have a bit of proof theory (e.g. for the saturation proofs) and universal algebra (and term rewriting specifically) to explain differences between the techniques, and I don't know how much of that is sensible to assume, also necessary for some of the constructions.

[Terence Tao]

I probably should have said this earlier, but I was thinking of submitting this paper, when it is completed, to the newly formed Annals of Formalized Mathematics. So the audience would be very diverse, ranging from experts in universal algebra at one end and experts in automated theorem proving or formal proof assistants at the other. Almost nobody would have expertise in all the areas covered in the project. So it would be good to keep the paper as accessible as possible. To that end, it would be helpful for people to review sections of the paper draft not in their area and point out places where the exposition is assuming expert knowledge, for instance by using a technical term without defining it or giving a suitable reference (in some cases we might be able to point to our own blueprint for more details).

[Jose Brox]

Terence Tao ha dicho:

I was thinking of submitting this paper, when it is completed, to the newly formed Annals of Formalized Mathematics.

I was wondering if we would try Nature and Science :grinning_face_with_smiling_eyes:

[Terence Tao]

It's possible that we may end up having multiple papers come out of this project, though for now I have just kept things as a single paper. The first Polymath project led to two mathematical papers (one in Annals of Math) but also several retrospective articles (including an opinion piece in Nature). If it turns out that we have a lot to say about collaborative math research projects built on a formalized foundation I could imagine that being a separate paper. Perhaps once we have a more developed "Conclusions" / "Reflections" section in the current draft, this will become clearer.

[Shreyas Srinivas]

Vlad Tsyrklevich said:

Just to be clear: the ability to 'claim' an issue is specific infrastructure for this project, not GitHub generally. The way it works is that only a single person can claim an issue, but you can think of this as a formality to avoid unwitting duplication of effort. There's nothing to stop you from working with others.

This is correct. I designed it based on how the previous outstanding tasks mechanism was intended to work. That being said collaboration is fine and has been happening quite a bit already.

You could also make dependent PRs if you wish.

[Shreyas Srinivas]

From the maintainers side, it also allows us to track who is working on a task and which PRs to accept, in case someone else isn't following the process.

[Jose Brox]

For the machine learning section, recall that Fernando Vaquerizo and myself trained a 4-layer CNN with the implication graph data, with 1% of the implications for the training set and another 1% for validation (1/1/98), the accuracy being 99.3%. On the other hand, @Adam Topaz used a vectorized model and a different way of producing the dataset, also with high accuracies.

Two experiments that we have not done yet (because I went to work on the remaining implications), but that we have talked about before in Zulip, and we can do easily and quickly are: 1) Try Adam's dataset on our CNN model and see how it performs, and 2) try our CNN model on the dataset of implications with the identities erased (just random numbers as labels) to see how much of the accuracy is due to the CNN learning transitivity, and not because of patterns in the identities.

I just wanted to check (@Terence Tao) that we should go ahead and perform these two experiments (I'd do the data conversion and Fernando the CNN training).

In any case, if we use any of these results from the CNN, I think Fernando Vaquerizo should be added as a coauthor (he is not in Zulip).

[Terence Tao]

That sounds good to me. Are the results comparable with the Graph ML section already in the paper that @Pietro Monticone uploaded? In particular, would there be a way to unify the discussions of these results?

[Shreyas Srinivas]

From my last recollection, the graph prediction algorithm was looking for patterns and predicting implications and anti-implications. I don't remember how this was tested and validated against the final implication graph

[Shreyas Srinivas]

Also, I am not sure how to interpret such a prediction

[Shreyas Srinivas]

What pattern is the algorithm seeing?

[Shreyas Srinivas]

Do we know for instance that the algorithm isn't finding a spurious pattern based on topological properties of the graph or the shapes of equations or some combination?

[Terence Tao]

Thanks to @Andrés Goens for writing the first draft of the "Proof Automation" section at equational#930! I encourage other contributors to review it, and I will merge it soon into the paper when the comments are incorporated and all the merge conflicts are resolved. I've not attempted to write a paper through github pull requests before, but I can see the value in it now; for any significant edits to the paper going forward I may also try to use the PR mechanism rather than just unilaterally editing the paper directly.

I am thinking of promoting the finite magma part of the project to the level of primary objective, so that the ETP main objective retroactively becomes determining both the general magma implication graph and the finite magma implication graph for the 4694 equations. I would probably introduce a symbol such as $\vdash_{\mathrm{fin}}$ to define finite entailment, and instead of having a separate section for the finite implications as the structure is currently, one would instead discuss both the general implication and finite implication simultaneously in each section (e.g., for each construction of counterexamples, indicate whether the counterexample is finite).

I'm also thinking of not having a "reflections" section in which individual contributors discuss their experiences, as this would make the paper somewhat self-referential (and also quite long). I was thinking instead when we finally declare "victory" for this project (a reasonable milestone for this would be when all the implications for both the infinite and finite graph are formalized in Lean) to collect such recollections, which perhaps could be a basis for a subsequent retrospective paper (along the lines of this retrospective Polymath paper).

Finally, if anyone has any general comments on the paper, e.g., if there are any topics that are currently not discussed in the draft but are worth mentioning, please mention them here.

[Andrés Goens]

yes, sorry I've been quite slow on this, but thanks for the comments (and also @Vlad Tsyrklevich ), I'll get to them soon! I guess the merge conflict is because the pdf is checked into the paper. Maybe it makes sense to delete it and have it be built in CI, like the blueprint?

[Terence Tao]

That sounds like a good idea, though I don't know how to implement the CI on a technical level. One can override the merge conflict and replace the pdf directly, but it would perhaps be better (particularly as more sections start coming in) to not have to deal with this issue with each PR.

[Pietro Monticone]

Isn’t it better to just .gitignore the main.pdf file?

[Andrés Goens]

but then people cannot just download the latest version without building it themselves

[Pietro Monticone]

Ok, I’ll write a paper.yml later today or tomorrow.

[Pietro Monticone]

But then we’ll need:

1. Contributors should not push the main.pdf in their PRs
2. The compile-paper workflow should be triggered only on push events to main and not on PR events

[Vlad Tsyrklevich]

If we're doing CI, maybe we .gitignore *.pdf and just put the paper.pdf in home_page?

[Pietro Monticone]

Yes exactly

[Vlad Tsyrklevich]

Ah ok, I thought you were saying keep the .pdfs on main

[Pietro Monticone]

I think is better to have a separate workflow file so that for [PAPER] contributions people don’t have to wait for whole blueprint to compile etc.

[Pietro Monticone]

I’ll also add a “Paper” button on the project website.

[Shreyas Srinivas]

If we push and share the gitignore, the issue goes away

[Shreyas Srinivas]

Another solution is to use overleaf, if someone has a professional or enterprise overleaf account

[Shreyas Srinivas]

Overleaf will save us a lot of trouble that might come from incompatible latex installations, packages etc

[Pietro Monticone]

I would stick to the mono-platform solution.

[Pietro Monticone]

Here is the associated task issue https://github.com/teorth/equational_theories/issues/989

[Andrés Goens]

a concrete point against overleaf in this case is that it would also remove the PR and review process, which in this case we probably want to keep

[Pietro Monticone]

Pietro Monticone said:

I think is better to have a separate workflow file so that for [PAPER] contributions people don’t have to wait for whole blueprint to compile etc.

Oh right, I cannot do that because GitHub Pages deployments overwrite the previously published site... I will integrate everything into a single "Compile blueprint and paper" workflow then.

[Pietro Monticone]

Done:

• PR https://github.com/teorth/equational_theories/pull/990
• Homepage: https://teorth.github.io/equational_theories/
• Paper: https://teorth.github.io/equational_theories/paper.pdf

[Pietro Monticone]

Resolved the conflict, fixed typos and merged main in equational#930.

[Shreyas Srinivas]

I am working towards a draft of the project management and explaining my design of the project process. Before I write it out fully (maybe a draft by Saturday night German time), I wanted to get some feedback and thoughts about how participants of the project felt about it. During the project we already accumulated a list of points to talk about and this can be seen in the draft notes. I want to get a sense of what worked, what didn't and what could have been better.

[Shreyas Srinivas]

On the paper draft this is section 4

[Shreyas Srinivas]

Also, since FLT is using a similar process @Kevin Buzzard : I would like to get your take on it so far

[Vlad Tsyrklevich]

One small thing I wished we had, was something like #rss for equational commits/issues/PRs. It could just be a single thread on Zulip instead of a whole channel, just announcing what happened without necessarily requiring the same level of detail. For those who care to keep track of what's going on, it just makes it a lot easier if it's pushed to a thread somewhere instead of looking multiple places on GitHub to keep track

[Shreyas Srinivas]

You mean over and above the project dashboard? Specifically, is it the linear feed of events that #rss channel provides?

[Vlad Tsyrklevich]

I guess I never used that dashboard much, it's busy and it also doesn't include commits without PRs. (Also, it would be nice if it reverse-sorted it's columns so you saw what was most-fresh instead of what is most-stale.)

Yes, I want a linear feed of events to make it easy to keep track of what others are doing.

[Vlad Tsyrklevich]

One nice consequence of this for the maintainers is that it may invite more PR feedback from other contributors.

[Terence Tao]

(By the way, the paper draft is now officially available from the dashboard, or at this link, thanks to some recent interface upgrades by @Pietro Monticone .)

Certainly from the perspective of the person issuing a large fraction of the tasks, I find the Github issues based system a marked improvement over the previous ad hoc system of manually updating a Zulip thread of tasks. Not all tasks are perfectly suited for the system - in particular the tasks that require a lot of ongoing discussion between a large number of project participants, such as attacking an equation for which the way forward is not yet clear - but for the ones in which the task can be safely assigned to a single participant, it seems to work well. At the same time, I appreciate the flexibility to also propose tasks and PRs (e.g., for correcting minor typos) outside of the formal issue system.

[Pietro Monticone]

Vlad Tsyrklevich said:

One small thing I wished we had, was something like #rss for equational commits/issues/PRs. It could just be a single thread on Zulip instead of a whole channel, just announcing what happened without necessarily requiring the same level of detail. For those who care to keep track of what's going on, it just makes it a lot easier if it's pushed to a thread somewhere instead of looking multiple places on GitHub to keep track

Wouldn’t the GitHub “Watch” feature suffice for this purpose? It provides customisable notifications for all activity on a repository, including commits, issues, and pull requests.

[Pietro Monticone]

Or we could have used a GitHub bot https://zulip.com/integrations/doc/github

[Vlad Tsyrklevich]

Pietro Monticone said:

Wouldn’t the GitHub “Watch” feature suffice for this purpose?

I suppose it could have, if I 1) had the mobile GitHub app installed, or 2) looked at GitHub regularly outside of submitting PRs/addressing feedback

[Vlad Tsyrklevich]

Regarding equational#923 (paper section for order 5 trivial/Austin laws), I wanted to solicit feedback on what I should do. I've run out of juice to keep pushing that effort any further. I've exhausted the basic methods of finding finite examples and finite implications for the remaining set of unknowns. I will briefly summarize the results as: Outside of equations with known finite models or with only trivial models, there are 3 sets of remaining (interesting) equations: 1) verified Austin laws (where their infinite non-triviality is derived from Vampire, not by formalization in Lean), 2) laws that are finite-trivial and it is unknown whether they have infinite models (these are likely Austin laws), and 3) 12 remaining equations for which I have been unable to find finite models or prove that they are trivial. (Note that 1 of these unknowns is known to have infinite models according to Vampire.)

This is the start of something interesting, but given that it's half-done and likely won't be pushed any further, I was unsure if it's worth documenting the current state. If it is, I'll gladly take it on, but I'd like to get feedback on whether it's worth reporting the partial progress.

[Terence Tao]

I think it's good to report the partial progress so that any future researcher can build upon it. If you don't feel like it's definitive enough to put in the paper, we can instead make a blueprint chapter for it and make a reference to that chapter in the paper (that way, even if the paper remains static, the blueprint chapter can be updated in the future with more progress, and the reference will remain current). Would you be more comfortable with that approach?

[Vlad Tsyrklevich]

I'm comfortable with either--I just don't feel qualified to make the call on where it belongs

[Terence Tao]

In that case why don't we aim for making a blueprint chapter for now? If there is unexpected progress on this front beyond the current state, we can always try to incorporate whatever you write into the paper itself, but the tentative plan would just be to state in the paper that some partial results are known on the order 5 question and refer the reader to the blueprint for the latest updates. I've modified the task at equational#923 to reflect this option.

[Harald Husum]

Just skimming though the paper now. I noticed that Chapter 8 starts out by stating:

85 laws have been shown to be equivalent to the constant law (Definition 2.20), and 815 laws
have been shown to be equivalent to the singleton law (Definition 2.2).

Shouldn't these numbers be 418 and 1495? Or am I missing some context?

[Terence Tao]

I think you are looking at the blueprint, which is distinct from the paper (which can be found at https://teorth.github.io/equational_theories/paper.pdf ).

Chapter 8 referred to a very early stage of the project (in the first few days, I think) in which we just started to implement some algorithms to prove equivalence with constant or singleton laws, for instance by locating laws of the form $x = f(y,z,w)$ (which are automatically equivalent to the singleton law). As you indicate, they are only a fraction of the total number of laws that are equivalent to these laws. The corresponding place in the paper where they should be mentioned is Section 6.1, although I didn't actually get around to putting those statistics yet.

[Harald Husum]

Yeah, you're right, it was the blueprint. Thank you for pointing me in the right direction. I got to the blueprint by clicking the paper badge on github; maybe we should point that to the actual paper instead.

Screenshot 2024-12-14 at 00.05.53.png

[Harald Husum]

https://github.com/teorth/equational_theories/pull/1024

[Jose Brox]

Are we still planning on finishing the paper for the end of the year? I propose to extend the provisional deadline, say, to the end of January. For my part, I'd like to write the first draft of the Higman-Neumann section, collaborate on the ATPs section, keep working on HN, work a little more on 677->255 before admitting defeat, and do a couple of neural network computations. And I'm going on vacation on December 22nd... There are too many things left to do and too little time to do them. I guess more people will be in a similar situation.

[Terence Tao]

Yeah, that end-of-year deadline in retrospect was far too optimistic, given that we haven't even formalized all the proofs in the main project yet. I'm also going on vacation soon, so perhaps Jan 31 will indeed be a more reasonable target at this stage.

[Shreyas Srinivas]

I apologise for the delays from my end. End of year deadline runs have been taking up all my time.

[Cody Roux]

I'm super late to the party, and my contributions were not substantial, but:

1. I wrote some things for the basic theory of rewriting, did we want to keep those?
2. I did write a couple lines for the completeness and compactness theorems. Should I add myself to https://github.com/teorth/equational_theories/blob/main/paper/contributions.md?

[Vlad Tsyrklevich]

Regarding 1, equational#926 is still open for writing about confluence/term rewriting in the paper itself (it looks like this is currently sections 6.3/6.4). Perhaps the text you contributed to the blueprint could be easily adapted to the paper?

[Terence Tao]

Yes, it would be great if someone with familiarity with confluence can contribute to the paper (and thus also to contributions.md), so feel free to list yourself as a contributor!

[Vlad Tsyrklevich]

I have a short 1-page section on user interfaces up for review at equational#1035 if anyone would like to provide feedback.

[Shreyas Srinivas]

While working on the paper draft, I noticed a number of notes to check later. Could we use the todonotes package and inline todonotes instead?

[Terence Tao]

Sure, feel free to implement this.

[Terence Tao]

The interfaces section looks good! It's probably about the right amount of detail - I thought about expanding more on the use cases of the interfaces, but they are all pretty self-explanatory, e.g., using FME as an immediate way to verify a finite magma produced by some theoretical construction (e.g., the cohomological construction).

[Cody Roux]

Ok, so I'm looking at writing the section on confluence: at the moment in the blueprint there are 2 such sections: https://teorth.github.io/equational_theories/blueprint/abstract-nonsense-chapter.html#a0000000039 and (my own) https://teorth.github.io/equational_theories/blueprint/rewriting-chapter.html.

Obviously it's tempting to adapt my own writing, since, well, it's my own writing. But I'd rather be consistent and uniform in style and notation, and I'd much rather refer to a lemma or theorem proven in the development than some other theorem in the literature (though they have also been machine checked _somewhere_).

However the definition in the former section confuses me a bit: defining a reduction as "does not increase the size of the term" seems non-standard, though I guess we're just picking the orientation that (weakly) decreases the length + lex of the equation. The "unique simplification" bit seems also a bit weird: are we ordering reductions? Here it feels like we need to operate on ground terms, otherwise the rule x + y -> y + x cannot get ordered.

[Cody Roux]

Note that in general, the "free theory" of a confluent system is not the set of normal forms, since there still is the possibility of terms without any normal form.

[Terence Tao]

I wrote the abstract nonsense chapter and at some point I decided to add some stuff about confluence, but I am not an expert on this topic and may have gotten the terminology and statements somewhat wrong here. Probably the material in Section 10.1 of the blueprint is a better fit for the term rewriting chapter anyway, so feel free to move it there and edit appropriately. I don't think that portion of the blueprint is directly connected to anything in the Lean codebase; there is some code (at Confluence.lean, Confluence1.lean, etc.) there establishing confluence but it is not connected to Section 10.1. It would make sense to align the discussion to that code (or your own rewriting chapter) rather than to Section 10.1 of the blueprint.

[Shreyas Srinivas]

@Pietro Monticone , could we get the todonotes package added to the CI runner?

[Pietro Monticone]

Just opened a draft PR equational#1039 to check whether the latest TeXLive-Full version works in our case.

[Pietro Monticone]

It worked. It should have solved all the packages-related issues.

Now it's ready to merge equational#1039

[Shreyas Srinivas]

Done