Terence Tao's personal log - teorth/equational_theories GitHub Wiki
Terence Tao's personal log on his experiences working on this project.
Day 1 (Sep 26)
The initial response has been quite enthusiastic, and the pace is significantly faster than I envisaged. The project is receiving a lot of technical support at the back end, and formalization and mathematical tasks are being completed extremely rapidly. Here I think this project has an advantage over other Lean projects in that the atomic tasks to complete are very small and most of them do not require extensive expertise in either Lean or math. It was important early on to have an agreed upon numbering system for the equations under study, which will hopefully stay stable for the duration of the primary goal of the project. Even refactoring eleven equations led to a lot of typos, I am glad I did not postpone the standardization of the numbering system until the project became far larger!
While automated tools, e.g., for autocompleting graph implications, will be absolutely necessary as the project scales larger, in the immediate term it seems that manual management of the project (e.g., through the now-standard "outstanding task" thread, and also through manual updating of the latest version of the Hasse diagram) is working for now. In the very short term, it's easier to deploy humans than to deploy automated tools. Having some API for Magma relations will eventually be helpful. We are already beginning to see some general statements about equational laws (e.g., the observation that any equation of the form x = f(y,z,w,u) is equivalent to the equation x=y) that might be worth formalizing, but with our current setup we can only handle a few equational laws at a time.
The existing infrastructure of github, zulip, blueprint, and also my blog, is holding up well so far. I anticipate some scaling issues as the project gets bigger, though.
This is perhaps invisible to other users, but I am finding Github Copilot very useful for the mundane task of entering in new Lean theorems to prove, or updating the blueprint to incorporate the latest PR'ed results. Basically it provides an easy way to translate between Lean and LaTeX: for instance to convert Lean to LaTeX I paste in the Lean code as a comment, start typing the LaTeX, and it usually autocompletes to what I want, particularly if several examples of similar text is already in the file. The text in both Lean and LaTeX is very standardized (to assist in machine readability), and this seems to increase the effectiveness of Github Copilot.
Day 2 (Sep 27)
This project has moved far, far quicker, and scaled up much much faster, than I had expected - only 48 hours in and already a large fraction of the implications are likely to be resolved soon! I thought the 3-week PFR project was fast, but this is an insane additional level of speed. It seems that projects that consist of extremely large numbers of independent pieces, each of which are easy to understand and attackable by a variety of methods, are a very good use case for these crowdsourced projects, and can really leverage the "wisdom of crowds" in ways that a highly centralized project cannot.
In particular, this is soon going to be a project that cannot be directed by just a small number of people; I think we will have to decentralize it into a loosely coordinated set of smaller groups working on different aspects of the problem. I am not sure exactly how we can facilitate that transition, but am looking forward to how the dynamics of the project evolve.
Automated tools to visualize the status of the project are going to be needed quite soon. Certainly the hand-drawn Hasse diagram that is supposed to guide the "outstanding tasks" is rapidly reaching the limits of usability.
Day 3 (Sep 28)
After an extremely hectic two days, things are beginning to stabilize. The new Github project/issues workflow to manage tasks like completing the subgraph of implications is significantly more convenient on my end than the older approach of manually updating an "Outstanding tasks" thread, which was becoming extraordinarily time-consuming. It is perhaps too early to say for certain, but at this point I would recommend other collaborative Lean projects transition over to a Github project for task management.
I wanted to highlight a very insightful comment on my blog from Tristan Stérin (founder of the BusyBeaver challenge) on how to manage these sorts of "high-entropy" crowdsourced formal projects.
Once we have automated tools to compile all the known implications and anti-implications from all submitted Lean files, and some way to display this data in various formats on the main web pages of the project, it seems that we can decentralize the operation of the project quite significantly; while some subprojects such as the Subgraph project would still require some central direction, I think we could be ready to open the door to arbitrary groups using arbitrary approaches to generate new portions of the implication graph, without the need for much coordination (other than what is listed in the new CONTRIBUTING.md file).
I am looking forward to seeing how the proof_wanted approach to capturing all non-Lean contributions to the implication graph (both human-generated and computer-generated) integrates with the Lean contributions (formalized via theorem rather than proof_wanted). Figuring out a viable general workflow to combine formal contributions, human contributions, and other computer-generated contributions (such as AI-generated contributions) has been one of my main motivations for this project.
Day 4 (Sep 29)
The project seems to be successfully decentralizing; in particular, there is now a lot of activity going on now that I am not fully aware of. This thread would be a good place for other participants to report on any progress not otherwise mentioned here, especially that which would be relevant to various other components of the project. (I guess this would be called a "stand-up meeting" in software engineering?)
For instance, I was delighted to recieve #116 from Franklin Dyer in which two old Putnam problems, which essentially asked to establish three implications between laws already in the database, were added to Subgraph.lean. I have since added them to the blueprint as well, and will also update the Hasse diagram accordingly.
As another spinoff activity, in #80 we managed to find a formula for the number of equational laws with n operations (up to relabeling, symmetry, and triviality), and will submit the resulting sequences to the OEIS. Technically this will be the first external output of this project! Also, since the proof of these formulae is already in the blueprint, I am planning to open some tasks to formalize their proofs in Lean, since the infrastructure to do so (as well as a suitable pool of contributors) is already in place...
Speaking of which, I certainly plan to write a paper on this project, probably submitted to a journal on formalized mathematics, which will discuss both the mathematical results of the project but also the workflow and experiences. This is still well into the future, after the primary goal of our project is completed, but I again encourage participants (or just casual observers) to share their impressions on this thread, as this may end up being part of the final paper. (See this similar retrospective paper on the Polymath8 project for a possible model.)
The task management workflow is now quite a painless experience for me, freeing up my time to deal with other aspects of the project, such as discussing how to transition smoothly from the current "semantic" Equation-based foundation of the project to a "syntactic" Law-based foundation. I am very grateful to the other moderators (Pietro Monticone , Shreyas Srinivas , and Joachim Breitner ) for taking the lead on running so much of the project!
Day 5 (Sep 30)
While there is plenty of activity on many fronts, it is beginning to decentralize quite smoothly, and I no longer feel like I have to be involved in most of the different directions here. I mostly have been focusing on some more theoretical aspects to the project, such as slowly setting out tasks for the metatheory of equations and for formalizing the counts for the number of equations.
We have already established enough easy implications from the original set of ~22 million that there are only ~3 million unsolved implications remaining (up to equivalence). I am expecting some contributions from AI-assisted efforts to start coming in soon, as well as large-scale automated proving runs. We have made a lot of progress in assembling a stable infrastructure to receive these sorts of new inputs, and I am looking forward to see how these (as well as other more elementary implication chasing methods) reduce the count further. Also, we now have some data sets online with which others can start performing some data visualization and/or data analysis; hopefully there will be some interesting features to the implication graph that we will start to see.
The number of distinct equational laws with n operations is now on the OEIS as A376640.
Day 6 (Oct 1)
Looks like we are getting most of the way to having an automated generation of implications, statistics, and visualizations set up, which will be useful both for contributors who want to conduct runs on the remaining outstanding implications, and also for more casual observers who could use some "eye candy" and quick summaries of progress. Also, I hope that now we have a few partial data sets, that some interesting data visualization and data analysis from new participants will emerge.
Much of the time I devoted to the project today was over "big-endian/little-endian" type issues, such as which orientation of ordering on laws (or Hasse diagrams) to use, or which symbol to use for the Magma operation. In informal mathematics these are utterly trivial problems, but for a formal project it is important to settle on a standard, and it is much easier to modify that standard early in the project rather than later. So this is the sort of task that has to happen now. I am finding the polling feature of Zulip to be useful for this, and hopefully this type of participation will help decentralize the project and help the contributors feel like they are active stakeholders.
I did have some speculation over at #Equational > Ideas for unknown implications regarding a possible future "assembly line" type workflow in which different teams work independently on sequentially connected components of the project, but perhaps we have not yet scaled up our infrastructure and participation to reach that point yet.
Day 7 (Oct 2)
Based on the polls, I requested one minor refactor of the codebase (reversing the order on laws), though this is relatively low priority and has not yet been implemented. The most striking progress today has been firstly on the front end, where we now have a nice dashboard for our results, and some significant new progress in whittling down the number of implications; at one point we thought we had achieved a huge reduction, proving or conjecturing 99.958% of all implications; while this was a reporting error, we still have a respectable 95% or so of implications resolved now once the most recent PRs resolve.
Another cute result in the literature is now formalized within the project: it turns out that Equation1571 is equivalent to being an abelian group of exponent 2 (which then obeys a whole slew of additional equations). This is an old result of Mendelsohn and Padmanabhan from 1975.
Day 8 (Oct 3)
Several contributions made the verified component of implications inch up to 87% or so, with a large PR of conjectural implications still in review. We now have a very nice experimental tool to explore the implication graph, which should help locate interesting areas of the graph to focus on to make further progress.
I've set up branch protection, and have had to learn the discipline of having to submit PRs and wait for CI like everyone else. It took some getting used to, but I think I have gotten the hang of it now, and presumably will stop regularly breaking the build going forward.
We rolled out the first major refactor today - a change in the magma operation symbol to make the Lean code compile significantly faster. Hopefully there will not be too many secondary impacts of this simple, but rather broad, change.
A future research question was resolved by Daniel Weber : it is now established (and proven in Lean in #244) that the implication Equation3994 -> Equation3588 is false, but that all counterexamples were infinite. This is an early example of the type of result that is enabled by this sort of systematic search, as this implication was flagged as a possible candidate via the Vampire run.
Day 9 (Oct 4)
Progress continues on several fronts. Most visibly, the completion rate of the implication graph is now an impressive 99.866%! (We will soon need more digits of precision on our percentage displays). This is largely thanks to the Vampire run, the positive implications of which have now been formalized in Lean. I'm very grateful to all the contributors who worked behind the scenes to build in mere days the infrastructure to efficiently accept large automated Lean contributions, reduce them to something that can be compiled by Lean in reasonable time, and interpret the output.
In fact I found myself with some surplus time for the first time in a week, as most components of the project are now proceeding more or less autonomously, and I could now just participate in the aspects where I felt I could make a contribution, rather than having to "put out fires".
Soon we will have exhausted most of the low hanging fruit, and it seems we will have about ten thousand challenging implications that are beyond the reach of automated provers or small finite magmas. This is where I expect the project to get more interesting, with human analysis of key examples becoming an important component. This is also a potential period in which AI assistance may also become useful.
There are some interesting discussions over at #Equational > Future directions on how one can use the increasingly complete data we have to explore other questions in universal algebra, and also some nascent attempts to experimentally probe the graph for insights. I am hoping we identify some anomalous structures centered around some equational laws that are mathematically interesting, but have not received much attention in previous literature.
I briefly mentioned this project in a recent interview (partially paywalled) at the Atlantic.
Day 10 (Oct 5)
I learned today about the wiki feature of a github repository, and so this personal log is moving from the Lean Zulip to the Github wiki.
The front web page is becoming increasingly user-friendly, I think. We now have an official implication explorer to explore the implication graph through a clickable web interface, which among other things now has a nice "Prove this!" feature next to any unsolved implication to be taken to a Lean playground with the statements to be proven. Many contributors are already using the explorer to identify "high-yield" implications that they can then attack with their favorite tools, whether it be theory or computer assistance. In this direction, I would like to highlight Zoltan Kocsis's account of how he directs Prover9 and Mace4 to "dig through" the most promising veins associated to the highest yield outstanding problems.
Spent significant time today on "meta" discussions, including whether to interpret the equation laws in the Type 0 universe, or arbitrary Type * universes. This is a technical model-theoretic discussion, but has some important implications in the "back end" of the Lean formalization, in particular our eventual switch to "deep" interpretation of equation implications based on syntax instead of semantics, which will for instance allow us to utilize the duality symmetry of the equation graph. We also had a very productive meta discussion on authorship structure of any future paper on this project, code of conduct issues, and security vulnerabilities. These are not issues I had thought much about when launching this project, but they are important, and especially ought to be discussed here if this project is to be viewed as a model for future large-scale collaborative mathematical projects.
The completion rate has ticked up to above 99%, with the production of finite counterexamples becoming more systematic and streamlined. However, at some point we will presumably have to turn to infinite, or large finite counterexamples to complete the graph. One promising proposal has just been introduced by Pace Nielsen here.
Day 11 (Oct 6)
Amusingly, a significant amount of progress was obtained mostly by fixing an accounting error - our count of missing implications counted some extra equations beyond the original 4694, and removing those lowered the outstanding implications to 1121 - or just 440 if we quotient out by equivalences and duality. The end is in sight, with the completion rate up to an impressive-looking 99.9957%! The linear magmas proposed yesterday have helped somewhat in getting this count down so low, though there are still many mysterious implications that are resistant to this approach. I expect the last few stubborn holdouts to be quite challenging to dislodge, although progress has proceeded to date far faster than I had anticipated, so I may well be surprised on this.
We have started a plan for the paper, and had some interesting discussions about authorship, with a tentative plan to use the CRediT categories (with our own interpretation and elaboration) in an appendix to list author's contributions. We also discussed the possibility of attaching a second Github repository to this project to coordinate the writing, but not to attempt to make any significant changes to the organizational structure of the current repository. (But if we were to do it all over again, we should probably have planned out the Github organizational structure and roles more thoughtfully.)
Thanks to Vlad Tsyrklevich, we now have a second (experimental) visualization tool: Graphiti, that lets one explore portions of the graph displayed as a Hasse diagram. Hopefully this will also get integrated nicely with our equation explorer to find an appealing way to understand the geometry of this space!
Day 12 (Oct 7)
Some slight movement in the completion statistics: the number of outstanding implications ticked downwards from 1121 to 999, with the linear magma counterexamples being formalized, and a few other implications resolved as well. A new approach by Fan Zheng, based on studying equational laws that are "confluent" (have unique simplification), looks like it will settle two dozen or more additional implications, particularly those concerning equation 477 and similar equations; see this thread. We will be working on formalizing these somewhat intricate arguments.
Meanwhile, equation 65 is proving stubborn to resolve (I compared it to the village of Asterix and Obelix: "One small village of indomitable Gauls still holds out against the invaders..."). The key seems to be understanding its relation to equation 1491. They are equivalent for finite or left-cancellative magmas, thus defeating a lot of counterexample constructions, but the infinite non-cancellative case remains mysterious. Here is where I think the project is forcing us to discover new mathematical techniques to resolve implications, which will be a great outcome of the project.
There was some quite insightful discussion about the different ways in which automated theorem provers (ATPs) can be used in these sorts of Lean-based collaborative projects. We have largely adopted the paradigm of using ATPs as external tools to generate first conjectures, then (somewhat opaque) auto-generated Lean proofs. However, in the long term having these ATPs incorporated into Lean as tactics (somewhat similar to what is done in other languages such as Isabelle) may be the better solution. It is also worth noting that the speed of the ATP paradigm may have come at the expense of developing some promising human-directed approaches to the subject, though I think now that the pure ATP approach is reaching its limits, and the remaining implications are becoming increasingly interesting, these other approaches are returning to prominence. One possible interesting development is to convert semi-automated approaches (in which a human directs automated tools in a semi-mechanical fashion) into more fully automated approaches with an additional layer of scripting: see this thread for discussion.
We're already beginning to see how the various tools can be used to work together. As displayed on our Equation Explorer, there are seven equations for which it is open whether equation 65 implies them. The simplest is 359, so our discussion has focused on whether 65 implies 359. However, after using our Graphiti tool to diagram these implications, it now appears that it is in fact the implication 65 => 1491, as well as its converse, which are the more critical implications to resolve. This will hopefully help direct future progress on this front.
Day 13 (Oct 8)
The heady days of order of magnitude improvement in the outstanding implications are likely over, but progress is still being made (and, on the plus side from the maintainer end, we are no longer running around desperately trying to ensure that the project management tools are scaling up with the project). The raw number of unresolved implications has been pared down to 950, largely thanks to increasing formalization of the anti-implications obtained from confluent laws - an idea introduced to the project by Fan Zheng, with some impressively rapid formalization by Joachim Breitner, and much further discussion on how to systematically exploit this idea. We also have an additional 200 or so anti-implications conjecturally resolved, due to a bug in previous Vampire runs (revealed upon retesting Vampire against the implications we are studying by hand) that caused those runs to skip some statements to check. After we quotient out by symmetries and duality, the number of independent statements we have to check drops down to roughly 300. (There is some overlap here with the confluent progress, as Vampire's methods often seem able to detect confluence.)
A third new web tool will soon be joining Equation Explorer and Graphiti: Zoltan Kocsis has released a prototype of Finite Magma Explorer, which takes a given finite magma and tell you what equations it studies. Already it is being used to close off some anti-implications that we conjectured to hold from duality considerations, but had not yet been able to get around to establishing rigorously. All three tools are still being developed and integrated, with a lot of feature requests being quite rapidly. We welcome feedback from casual observers!
Equations 65 and 1491, which I have nicknamed "Asterix" and "Obelix" respectively, continue to defy theoretical understanding. They exhibit no confluence properties, and cannot be distinguished by finite or linear magmas, but do have non-trivial models, such as x ◇ y = ω x in a field that contains a cube root of unity ω, or x ◇ y = y + 1 in the cyclic group of order 3. It is slowly emerging that left-cancellability is the key: for instance, assuming "Asterix", the equation "Obelix" is in fact equivalent to left-cancellability. Vampire is being deployed to see what are the consequences of left-cancellability failing, but so far the results are inconclusive.
We've had some discussion on what the ideal collaboration platform for such projects might look like in the future. While there are some potential useful new features, such as a specialized Lean playground (possibly run within a remote Gitpod) to allow casual participants to work with small fragments of the projects, such as formalizing a single lemma, there is a feeling that the current Github framework is largely "good enough", and somewhat difficult to compete with at this point from a software platform built from scratch.
Modern AI tools, so far, are the "dog that didn't bark in the night". We are making major use of "good old-fashioned AI", in the form of automated theorem provers such as Vampire; but the primary use cases of more modern large language models or other machine learning-based software thus far have been Github Copilot (to speed up writing code and Lean proofs through AI-powered autocomplete), and Claude (to help create our visualization tools, most notably Equation Explorer, which Claude charmingly named "Advanced Equation Implication Table" initially). I have also found ChatGPT to be useful for getting me up to speed on the finer aspects of universal algebra. I have been told from a major AI company in the first few days of the project that their tools were able to resolve a large fraction (over 99.9%) of the implications, but with quite long and inelegant proofs. But now that we have isolated some particularly challenging problems, I believe these AI tools will become more relevant.
Day 14 (Oct 9)
We have not yet set up an automated log of the dashboard stats, so I had been manually recording them on the front page, but I guess this is a better place to manually store them for now.
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 30515 | 8147764 | 582132 | 13272284 | 941 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 197 | 12 | 732 |
So, the progress is inching forward, mostly by formalizing more of the confluence constructions obtained previously, and recording the results of Vampire's saturation-based counterexamples as conjectures. It has been proposed in fact that all outstanding implications are in fact false, though perhaps there are some implications left out there with enormous proofs that are too unusual to be picked up by automated theorem provers.
There is finally a breakthrough on the siege of the "Asterix and Obelix" cluster (or "village"?) of laws: we now know (subject to checking) that the "Asterix" law 65 does not imply the "Obelix" law 1491! The proof is recorded in the blueprint and discusssed here. Daniel Weber has observed some minor issues with the argument, but has also proposed fixes and other improvements, and has offered to take the lead on formalizing this anti-implication. The method is based on first implementing a translation-invariant ansatz (reducing the problem to one resembling an IMO "functional equation" problem) and then solving that ansatz by a modified greedy algorithm on an infinite domain (we choose the integers, although pretty much any infinite abelian group without 2-torsion would have sufficed). The method looks flexible and hopefully it can resolve the other open implications in this cluster, and perhaps also in related clusters.
We are encountering a technical issue that is slowing down our work - at some point, the codebase became extremely lengthy to compile (50 minutes in some cases). This is one scaling issue that comes with large formalization projects; when the codebase is massive and largely automated, it is not enough for every contribution to compile; efficiency of compile time becomes a concern. This thread is devoted to tracking down the issue and resolving it. While the process is still ongoing, I am very pleased to see that it is progressing without any active involvement on my part; apart from having Pietro and Shreyas as collaborators on the Github project to approve pull requests and perform maintainance, the contributors of this project have largely self-coordinated to perform various specialized subtasks of which I have only the barest direct interaction with. For instance, all of the wonderful new visualization tools were developed by project volunteers; I offered some feedback on suggested additions to the user interface, but definitely did not micromanage the tasks. Similarly, I have not actually touched any Lean code in over a week (other than for the barest of housekeeping, like moving a definition from one file to another); the formalization side of the project has largely been self-coordinated by relevant volunteers. So the project is decentralizing more or less as I had hoped it would in its early days.
I am also pleased to see a very broad range of contributors, ranging from professional researchers and graduate students in mathematics or computer science, to various people from other professions with an undergraduate level of mathematics education. This is one of the key advantages of a highly structured collaborative project - there are modular subtasks in the project that can be usefully contributed to by someone who does not necessarily have the complete set of skills needed to understand the entire project. At one end, we are getting important insights from senior mathematicians with no prior expertise in Lean; we are getting volunteers to formalize a single theorem stated in the blueprint that requires only a relatively narrow amount of mathematical expertise; and we are getting a lot of invaluable technical support in maintaining the Github backend and various user interface front-ends that require little experience with either advanced mathematics or Lean. Certainly most of the contributions coming in now are well outside of what I can readily produce with my own skill set, and it has been a real pleasure seeing the project far outgrow my own initial contributions.
Day 15 (Oct 10)
We will soon be setting up automated logging of statistics (and even backfilling from previous days, thanks to the magic of github rollbacks). Nevertheless, here is the current snapshot of progress.
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 30515 | 8147764 | 582139 | 13272286 | 932 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 190 | 10 | 732 |
So, a relatively modest gain over yesterday, in which some of the conjectural anti-implications from Vampire were formalized. However, progress is still advancing on other fronts; the recent breakthrough in the Asterix/Obelix cluster should soon be formalized, although there are some unexpected obstructions in using the technique to resolve the other anti-implications. Separately, an infinite magma (a modification of a translation-invariant magma) was recently constructed by Zoltan Kocsis to resolve another anti-implication, with some hope that this method will generalize to handle others.
The issue leading to major slowdowns in build times has been identified, and a fix has been implemented. Unfortunately, the fix (which involved splitting up one of the core files AllEquations.lean into smaller files) caused some secondary issues, but these are also being fixed as well. I was busy with other commitments for most of yesterday, but I was very pleased to see that the rest of the project community was able to come together and resolve these issues with close to zero involvement on my part.
These secondary issues, by the way, were caused by fragility in one of our early design choices, which was to make two lean files, AllEquations.lean and Equations.lean, the "ground truth" for recording all the equations that the project satisfies. This was convenient at the time, since these files already existed and were the core of our Lean codebase. However it meant that any changes to these files, such as splitting up the former, or removing an equation of the latter, corrupted several of our visualization tools. We are slowly refactoring these tools to instead generate a JSON file of equations as the ground truth, and have all tools draw from that file. These sort of "back end" issues are hard to anticipate (and at the start of the project, when the codebase is still small and many of the tools hypothetical, implementing these sorts of data flows feels like overengineering). But it seems that it is possible to keep refactoring the codebase as one progresses, though if the project gets significantly more complex then I could imagine that this becomes increasingly difficult (I believe this problem is what is referred to in the software industry as "technical debt").
The "age of automated theorem provers" in this project appears to be coming to a close. Now the focus is returning to human-generated arguments for specific equations, with secondary efforts to generalize such individual proofs to larger classes of equations. Hopefully automation can still help with the second task at least, but it is interesting to see the significant shift in focus and activity as we move from one phase of the project to the next.
Day 16 (Oct 11)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582156 | 13272313 | 888 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 174 | 10 | 704 |
A lot of exciting progress, some of which is just now being formalized and will not show up in the above headline statistics for a day or two. On the technical side, the number of explicit implications proven was transitively reduced by Vlad Tsyrklevich, from 30,515 to 10,657, to improve compile times. The confluence-based conjectures continue to be formalized at a steady pace, thanks to contributions by Amir Livne Bar-on, lyphyser, and others. Several variants of the "Asterix !-> Obelix" anti-implication have been discovered by Daniel Weber and Pace Nielsen, potentially resolving at least a hundred anti-implications (after applying duality) and there is hope that these sorts of arguments can be partially or fully automated. Separately, Zoltan Kocsis has introduced a class of "modified translation-invariant models" that also have created some new anti-implications, for instance starting from 1661, and looks promisingly generalizable and automatable. And, building on his earlier contributions understanding the central groupoid law 168, Bhavik Mehta has shown that some laws (such as 2126) admit complete sets of rewriting rules despite not being confluent, and again there are prospects of automating these as well. So a lot of the outstanding implications look very attackable in the near term.
Day 17 (Oct 12)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582133 | 13272398 | 826 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 233 | 16 | 577 |
Steady progress on all previously reported fronts: the four methods previously discovered ("forcing" style infinite models, "modified translation-invariant models", "confluent law" verification, and "complete sets of rewriting rules") are in the process of being understood, (partially) automated, and deployed to various outstanding implications. At this point it is not clear exactly how many of the outstanding implications will be resolved by these methods, but thus far we are seeing promising reductions in the raw counts. (There will also be some cheap gains to be made once we have a good enough duality metatheory.) Other methods are still being explored, such as *-linear constructions or invariant-based arguments; so far, though, it seems that these arguments do not appear to rule out any additional implications, although they could provide simpler proofs of existing anti-implications.
Other than that, things are relatively quiet, with discussions about minor issues such as an uncontroversial renaming of a particular operation we defined in Lean, and how to systematically benchmark and compare the techniques we have developed over the course of the project. But after the hectic pace of the last few weeks, a lessening of excitement is actually somewhat welcome...
Day 18 (Oct 13)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582269 | 13272518 | 570 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 7 | 15 | 548 |
Our transitive closure algorithm now incorporates duality, permitting several duals of known results to be upgraded from "conjectured" to "proven", and we have also explicitly added as conjectures some results that had been worked out informally on the Lean Zulip. Daniel Weber is figuring out how to automate the greedy-algorithm technique that was successful in understanding the "Asterix" equation 65 (as well as some similar equations, namely 73, 1076, and the "Obelix" equation 1491), though the automated code we are employing is not optimal yet. Meanwhile, a modification of the greedy approach was discovered by Pace Nielsen that looks like it gives the anti-implication "Obelix does not imply Asterix", finishing off the entire Asterix-related cluster of problems.
It seemed like the right time to put out a blog post describing our progress so far. Among other things, this prompted a new discussion on how to incorporate machine learning tools into the project, with some interesting proposals already floated. The blog post has already also indirectly inspired a new Wikipedia article on central groupoids (equation 168, in our numbering system).
One random observation: this project requires a combination of quite distinct, but essential, components: online collaborative research (in the style of "Polymath", but in this case conducted via the Lean Zulip) + formal verification (Lean) + modern project management tools (Github) + data visualization tools (Graphviz + homebrewed tools) + automation (mostly automated theorem provers and back end data management, for us) + broad and diverse participation (academic/non-academic, junior/senior, math/CS/software engineering, etc.) + community standards (which we mostly codify using CONTRIBUTING.md). Previous projects had some subset of these components, but not all; and our project would be nowhere near as effective (or perhaps completely infeasible) if one or more of these components was removed. (Still waiting for the "+AI" component of the equation, though. For projects even larger than this, I expect to also see a "+funding" term.)
Day 19 (Oct 14)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582279 | 13272538 | 540 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 7 | 15 | 518 |
Only modest movement in the topline stats, but a lot of progress coming down the line. Bernard Reinke has used a simple translation-invariant magma to disprove some open anti-implications from 1648. It also looks like 1659 might be non-trivially confluent, using an infinite system of rewriting rules, as worked out through discussion between lyphyser, Daniel Weber, Fan Zheng, Bhavik Mehta, and ChatGPT - thus potentially being an actual direct use of modern AI in the research side of the project. Zoltan Kocsis has separately resolved the implications from 1659 by the modified translation invariant magma approach, and plans to use it as a model example of the method in the forthcoming blueprint chapter on this approach. And Daniel Weber has managed to automate the greedy algorithm approach, and tested it on the 36 outstanding hypothesis equations (up to equivalence and duality), and it appears to work for about 15 of them. The automation does not yet produce Lean code, but it should at least generate conjectures on the dashboard soon. So I expect a lot of movement by tomorrow!
An interesting numerical coincidence has been spotted, now that we have enough of the implication graph completed to notice it: there are "twin" equations, such as 124 and 1119, which imply and are implied by exactly the same set of equations, but are not equivalent or dual to each other. At present we have no plausible explanation for this phenomenon. I am hoping that there will be more of these "experimental mathematics" discoveries emerging in the future, though of course it would be good to completely resolve the implication graph first.
Speaking of which, we have just launched a "betting pool" (in the form of a poll) on what the implication graph will look like in a year: will all outstanding implications resolve to false, will there be a few holdouts (or a lot of holdouts), or some deep positive implication that all previous methods have missed? All are welcome to come "place a bet"!
Some interesting further suggestions have been made on how machine learning could be deployed on this project going forward. There was also a nice discussion on whether this project (or future, even larger-scale projects) could at some point be hosted on a managed graph database service such as Neptune, although this would require either funding or donated credits.
Day 20 (Oct 15)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582314 | 13272679 | 364 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 26 | 64 | 274 |
A significant chunk of the progress made in recent days has been either formalized or explicitly stated as a conjecture, leading to a sizeable reduction in the headline count of outstanding statistics. And more is to come: Daniel Weber has almost completed his automated run of greedy algorithm approaches to the outstanding equations, and identified ten new equations which should be completely resolvable by these techniques. There are also an additional three equations (713, 1289, and 1447) with an interesting new phenomenon - the greedy algorithm for these equations does close, but only barely, with a sizeable SAT-solver calculation required. This may create proofs of anti-implications (or possibly even implications, which would go against our current conventional wisdom) that are so long that it would be non-trivial to formalize and verify them in Lean! It will be interesting to see what happens with these three equations.
The mysterious "twinning" phenomenon alluded to yesterday is being explored further by Vlad Tsyrklevich and others. There is both numerical and theoretical evidence to suspect that this phenomenon is at least partly an artefact of our truncation of the implication graph to short laws, but something is still going on that we don't understand here.
Several further ideas for applying machine learning to this project were proposed by many participants. It will take time to implement most of these suggestions, but some efforts are now underway.
Bernard Reinke has discovered a non-abelian version of the translation-invariant magma construction, which looks like it disproves the implication 206 => 1648, and can be interpreted geometrically in terms of an infinite planar 3-regular graph. This particular anti-implication is also on track to be established by the automated greedy algorithm method, but this alternate construction may be more human-comprehensible and suggest approaches for remaining unresolved implications. This is similar to my experience in mathematical research as a whole: one technique may the first to solve problem X, but this by no means invalidates other approaches to solve the same problem, as often the different techniques generalize in different ways, or generate different insights, perspectives, or conceptual frameworks for these class of problems.
Michael Bucko is experimenting with ways to visualize the Lean codebase. It's still being tinkered with - much of the codebase is automatically generated and reduced, and these processes may create artefacts in the visualization - but there could well be insights (or at least some pleasing "eye candy") to come out of such visualizations.
Zoltan Kocsis, who contributed hugely to this project already, has had to step away for a few weeks to focus on other obligations. He wrote a very nice record of his impressions working on the project, which I recommend reading.
Day 21 (Oct 16)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582315 | 13272680 | 362 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 71 | 111 | 180 |
Most of the headline progress today comes from Daniel Weber completing the automated runs of the greedy algorithm method, which knocked out a large fraction of the remaining implications (conjecturally at least), and Joachim Breitner, who formalized Reinke's tree-based construction. At the time of writing, only nineteen equations (up to equivalence and duality) remain to be analyzed for this project! There is already an advance on two of them, the "Dupont/Dupond" pair 63/1692 (a variant of the Asterix/Obelix pair 65/1491); Pace Nielsen has just completed a modification of the (translation-invariant) greedy algorithm approach which looks like it can resolve the 24 implications stemming from this pair (and its duals). Bernard Reinke is also making some preliminary progress on another outstanding implication 1841->203.
We have started collecting together the "bag of tricks" for analyzing equations that we have acquired in the course of this project; this will likely become a section in our paper.
Vlad Tsyrklevich has pointed out that we are not systematically recording ways to replicate our automated results. This had not been a previous consideration, since in my mind at least the main "product" of the project was to be the Lean-formalized implication graph, rather than the code used to generate it; however, the processes used to generate that graph have been at least as interesting as the graph itself. We will need to have further discussion on this point.
One small observation: this project has often been moving too fast for the blueprint to catch up. In past formalization projects, typically one contributor would write a human-readable version of a lemma and its proof in the blueprint, another may then formalize the statement of the lemma in a Lean file, and a third contributor may then formalize the proof. Here, the pace is such that when a human-discovered proof of an implication is found, there are volunteers to immediately state and prove it in Lean, bypassing the blueprint altogether, or alternatively updating the blueprint some time after the formalization. This is perhaps an inevitable consequence of this project being about discovering new theorems rather than formalizing existing ones, but it is interesting to note the change in workflow as a consequence.
Day 22 (Oct 17)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582315 | 13272680 | 362 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 90 | 140 | 132 |
A relatively quiet day today. Daniel Weber's greedy algorithm run has now been fully implemented on the conjectural level, and we do not expect any further progress from a "pure" greedy approach in which we try to fill in the multiplication table one entry at a time, making the minimum number of changes needed at each step. However, Pace Nielsen's "modified" greedy approach, mentioned yesterday, remains a promising approach to resolve future implications (although one of the previous instances of this approach required some technical corrections). Meanwhile, Bernhard Reinke has extended his nonabelian translation invariant approach to obtain another anti-implication (though this one also be covered by the greedy approach).
The "highest yield" equation remaining is 1485; resolving this equation would settle 38 implications after duality. A preliminary thread for attacking it has been launched here. On the one hand, it has three variables, which seems to make it impervious to most of our previous techniques, which generally only work for equations with one or two variables. On the other hand, it is a weaker version of the central groupoid law 168, which is fairly well understood, so perhaps we will need to adapt some techniques from that literature.
There was some discussion (here and here) about what the final state of the equational graph should be. Right now only a fraction of the graph is explicitly formalized in Lean; most of it is "implicitly" recovered from the explicit portion through transitivity and duality. But a fully explicit formalization may be a desirable end goal, if we can figure out how to "compress" the Lean formalization efficiently enough that it can still compile in a reasonable amount of time.
Day 23 (Oct 18)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582315 | 13272680 | 362 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 91 | 141 | 130 |
Another slow day; Bernard Reinke used the infinite tree construction to (conjecturally) settle one more anti-implication, and hence its dual, but otherwise there has been no movement in the headline stats, although I expect a big transfer from the "conjectured" category to the "proved" category when the large tranche of implications currently conjecturally falsified by Daniel Weber's automated greedy algorithm becomes formalized into Lean.
Speaking of which, there is now some debate as to whether the term "conjecture" is the appropriate one to describe results that have been informally proved, or proved by some non-Lean computer code, but have not yet been formalized in Lean. This terminology was selected semi-arbitrarily about two weeks ago, but perhaps it is time to revisit it.
Joe McCann has volunteered to make various enhancements to our primary "Equation Explorer" visualization tool, which is already acquiring some nice new features, such as the ability to export statistics of the graph to a CSV file.
A little bit of progress on the highest-yield target of 1485; it has an intriguing graph-theoretic interpretation in terms of directed graphs with some special paths of length two, and a special axiom relating to cycles of length five. Will Sawin suggests that we should now look for directed graphs with few five-cycles to find interesting classes of examples. Hopefully more progress will be made on this front.
Day 24 (Oct 19)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582316 | 13272681 | 360 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 92 | 142 | 126 |
Progress is inching forward. Bernhard Reinke formalized the anti-implication that was informally obtained yesterday, and Pace Nielsen and I independently resolved the "Dupont !=> Dupond" anti-implication, at least informally, though the proof could conceivably be simplified. Pace also found a non-commutative translation-invariant greedy construction to (informally) resolve a further implication.
There was some extensive discussion on how one should convert from equations to laws and vice versa, and how this interacts with type universe issues. Now that the implication graph is almost complete, some of these issues have become almost moot, but they remain relevant for the long-term goal of obtaining an exportable "final state" of the implication graph and its Lean justification, which also has its own ongoing discussion.
Some more additions to the blueprint recently, most notably Cody Roux's contribution of a chapter on rewriting theories, and Zoltan Kocsis's contribution on infinite magma constructions (which also incorporates material from some chapters from previous versions of the blueprint.
A few additional examples and observations were made on "weak central groupoids" (1485), but we are still far from obtaining a good understanding of these objects, and in particular constructing more exampes of such magmas that could be used to disprove several open outstanding implications.
Some machine learning tools have been applied to the (nearly complete) implication graph, and it does appear that the graph is largely learnable by a convolutional neural network. It is not clear yet what features of the graph are being used by the network to discover it, though.
Day 25 (Oct 20)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582359 | 13272726 | 272 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 60 | 108 | 104 |
After three days of relatively little movement, there were a lot of visible developments on the dashboard today. Daniel Weber managed to complete the formalized version of his automated greedy algorithm, moving a large chunk of anti-implications from the "conjectured" category to the "proven" one. Furthermore, we have now systematically started to attack the 15 remaining equations (modulo equivalence and duality) with unresolved outbound implications, categorizing them by difficulty (and "immunity" to several existing techniques), and already made substantial progress, completely resolving three of them (one of which has already been formalized by Daniel Weber!) and partially resolving a fourth, thanks to extensive efforts by Pace Nielsen and others.
The remaining "battlefield" has shrunk to the point where we can completely describe it as follows.
- We have four (presumably quite challenging) equations in three variables to understand, including the weak central groupoid law 1485, for which we still only have a very partial understanding (though perhaps translation-invariant models hold some promise), as well as three additional equations 854, 1117, 1437 that we have not analyzed much yet.
- We have a newly discovered cluster of six equations that I have dubbed the "Hardy-Ramanujan cluster", inspired by the numerical coincidence that one of these equations, "Ramanujan", is numbered with Ramanujan's taxicab number 1729. At this time of writing, three of these equations are resolved, including two companions of "Ramanujan" which I have called "Hardy" (917) and "Littlewood" (2541), but three remain open, including "Ramanujan". The relation between Ramanujan, Hardy, and Littlewood is summarized here: Ramanujan implies Littlewood for all magmas, implies Hardy for translation-invariant magmas, and is equivalent to both Hardy and Littlewood for finite magmas. The other three equations 1323, 1526, 2744 in this cluster (which we have not given nicknames as of yet) are "mirror images" of the Hardy-Ramanujan-Littlewood trio, and would presumably be treatable by similar methods.
- Finally, we have five miscellaneous two-variable equations 1722, 1518, 1516, 3352, 3475 that we are currently attacking. One of these (1518) is unfortunately known to to be immune to translation-invariant methods, but the other four look susceptible. We also have discovered a new "ad hoc" method of using mostly constant magmas to attack equations obeyed by a globally constant magma (this is a variant of the "modified translation invariant models" considered in the past); it has resolved one equation so far, and it might handle one or two more.
Besides the visible dashboard progress, there has also been some advances on formalizing other theoretical results. Jérémy Scanvic formalized an old result of Austin that shows that two-variable equations cannot be "Austin models": they either only have trivial solutions, or have at least one non-trivial finite model. Anand Rao formalized more of the theory of lifting magma families, in particular relating them to a previously formalized construction of free magmas subject to a theory.
There was more extensive discussion on how best to formalize the "end-to-end" final theorem in Lean, with some productive technical discussion on how to efficiently verify that an implication graph is complete with a minimal amount of inputs and compute.
The Polynomial Freiman-Ruzsa (PFR) project took 23 days to achieve its primary goal of formalizing the proof of Marton's PFR conjecture, though it is still moving forward (much more slowly) a year after its initial launch with some tertiary goals (having achieved secondary goals of formalizing some variants and consequences of the PFR conjecture). Now that it is 25 days after the launch of the Equational Theories (ET) project, I thought it appropriate to make some comparisons between the two projects at comparable stages of time.
- Most obviously, in contrast to PFR, ET has not quite completed its primary goal; the dashboard shows that the formalization of the graph is 99.9988% complete and the informal description of the graph is 99.9995% complete, but these impressive statistics are somewhat misleading as the last few surviving implications are extremely stubborn, having resisted (or even being immune to) almost all of our previous techniques. Of course, the goal of Equational Theories was to discover and then formalize (22 million) new theorems, as opposed to PFR which aimed to formalize an existing theorem. So in this regard I view this current project as extremely successful to date.
- ET is a somewhat larger project than PFR, but not massively so. We currently have 40 github contributors to ET, compared to 30 for PFR. We currently have about 1,000 commits to ET after 25 days; it is difficult to make comparisons to PFR due to our different commit workflow, but after a year and three separate goals we are around 1,500 commits to PFR. Certainly the pace feels higher, though. [One small sample point in this direction: while writing this log entry, I had to wait for about an hour before there was enough of a gap between consecutive commits that the continuous integration (CI) for the entire project could actually complete and serve me the most updated dashboard statistics!]
- On the other hand, ET is massively computer-assisted, whereas very little automation was implemented for PFR. The overwhelming majority of the implications in ET established arose from reasonably sophisticated automated tools, such as automated theorem provers; in contrast, nearly all of the PFR codebase was written by hand (with a small amount of assistance from Github Copilot and similar tools).
- Much of the early discussion on PFR was on how to set up foundational theory for such fundamental concepts as Shannon entropy. We did have similar foundational debates (most notably regarding the distinction between equations and laws), but fortunately we could get going immediately on proving implications using a bare-bones implentation of magmas and equations, and defer the integration of those results to more sophisticated Lean-coded foundations later. As such, we had fewer bottlenecks than PFR.
- The workflow in PFR was managed by hand, in particular through pioneering the "Outstanding tasks" Zulip thread system of task management. This rapidly proved unworkable in ET and we switched early on to a more sophisticated Github project-based system, that has worked well so far. Though, as we close in on the last final equations and need to collate a lot of information outside of the formal Github repository, I have revived an "Outstanding equations" version of the old system to manage this (though now in coordination with some Github tracking issues).
- The PFR participants were primarily Lean programming enthusiasts. We of course have a significant fraction of such participants in ET, but we also have professional mathematicians with little prior Lean experience, as well as experts in automated theorem proving, user interfaces, data management, and machine learning. I find the conversations on the Zulip to be quite rich and diverse as a consequence.
Day 26 (Oct 21)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582365 | 13272742 | 250 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 109 | 82 |
Another day of significant progress on the headline dashboard. After a systematic assault on the fifteen outstanding equations by Daniel Weber, Pace Nielsen, Jose Brox, Bernhard Reinke, and others, ten of the equations are fully solved, two are partially solved, and three remain unscathed, though now we have understood what "immunities" most of the remaining equations have to our array of techniques; for instance, of the five equations, none of them can be resolved by commutative or noncommutative linear methods, and three are known to be immune to translation invariant methods, one is known to be immune to commutative constructions, and two are known to be immune to finite magma constructions. This knowledge of immunities has helped tremendously with "weapon selection" for these problems: many of the equations without translation-invariant immunities fell to a greedy translation-invariant approach, for instance, and one equation without linear immunity fell to a noncommutative linear construction. But perhaps the most interesting story was that of equation 3352, which had survived previous brute force finite magma searches involving small magmas (of order 4 or 5 at most), as well as a time-limited Vampire attack, but was not actually known to be immune to finite magma counterexamples. Daniel Weber had the key insight that through a theoretical analysis, it was possible to reduce to magmas for which the squaring map x ↦ x ◇ x was known to be injective. If one added this as an explicit axiom to automated theorem provers such as Vampire or Mace9, a finite counterexample was constructed in a fraction of a second; but without this axiom, Vampire took as long as a minute to locate a similar counterexample, so the theoretical insight led to a 100x speedup in Vampire's algorithm. This raises hopes that some of the remaining equations that are not yet known to be immune to finite magma examples could be attacked by some combination of automated theorem proving and human insight. Already, one of the most difficult-looking equations was partially solved by systematically testing Vampire with large time-outs on the equation. Also some of the outstanding equations was solved by surprisingly simple "ad hoc" constructions, such as small modifications of the constant magma operation or other similarly simple base model, so we have not completely exhausted elementary approaches in this project.
Some other developments to report. Pietro Monticone is slowly migrating some of the technical lemmas we developed during this project to Mathlib. Douglas McNeil contributed some nice heat map visualizations that showed how strongly the implication graph is biased against having equations with few variables imply equations with many variables; for instance, equations of one variable only imply equations of many variables when the latter can be reduced to the former by obvious substitution (this is likely a manifestation of confluence). Meanwhile, progress is being made on understanding why the implication poset is so readily learned by convolutional neural networks, although the findings are still not yet definitive.
It has been proposed to extend this project to also figure out what implications are known to be true or false when restricting only to finite magmas. We have a small number of "Austin pair" examples where an implication holds for finite magmas, but fails for infinite magmas; and many of our techniques to attack the toughest equations are genuinely infinitary in nature. So this extension is likely to be much more challenging to resolve than the original project, but there seems to be a good chance that we can at least mark the finite counterexamples in the Lean codebase as such, and obtain a reasonably near-complete version of the finite magma implication graph relatively soon.
Weak central groupoids (equation 1485) seem to be emerging as the "final boss" of the initial phase of the project. As the other equations are being resolved, I expect quite a bit of attention to be drawn to this equation soon, but for now our results are very preliminary.
Day 27 (Oct 22)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 582365 | 13272742 | 250 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 69 | 123 | 58 |
The dashboard has improved, but this is mostly for technical reasons (some of the progress noted yesterday was not properly recorded as a conjecture). Actually, we temporarily had negative progress on the project: the proof I had claimed for one of the equations (3485) turned out to have a gap, as was discovered by Daniel Weber when he tried to formalize my argument and found that I had omitted a key step in my case analysis. In fact I later worked out from this that my entire approach was obstructed. However, mere hours after this setback, Douglas McNeil found a finite counterexample to obtain this anti-implication, by guided use of automatic theorem provers. This guided ATP approach has proven surprisingly useful in this late stage of the project, and we are beginning to make more use of it in attacking the three of the five remaining equations that are not known to be immune to finite magma attacks. For instance, for the "final boss" of the weak central groupoid law, we now have a large class of order 8 magma examples which, while not yet creating any new anti-implications, are giving us useful insights as to what the structure of such magmas should look like. I am pleased to see more "experimental mathematics" approaches come into play here, in which we make empirical observations about the various finite magmas uncovered by automatic searches, and test these hypotheses against both theory and experiment.
There were some technical discussions involving the porting to Mathlib, and an unfortunate numbering error for one of the sporadic equations which has now been resolved. Michael Bucko and Eric Taucher have been experimenting with new ways to visualize the implication graph.
Day 28 (Oct 23)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586831 | 13268286 | 240 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 65 | 119 | 56 |
The main movement on the dashboard here is to input the recently discovered finite magma counterexamples into the Lean codebase; this input procedure is mostly automated, but there were some temporary glitches on the manual side as we had not actually used this procedure before.
We split up our discussion into threads focusing on individual equations. Two of them (1729 "Ramanujan" and 1323) are being studied via traditional "slow individual" means by Shreyas Srinivas and Bernhard Reinke, who will report on their progress in due course. The other three are being attacked by the complementary "fast collaborative" approach:
- For weak central groupoids (1485), the thread has reported significant progress thanks to the combined efforts of Jose Brox, Pace Nielsen, Bhavik Mehta, Kevin M, thormikkel, Ian Duleba, Daniel Weber, Michael Bucko, and others: we now understand the new order 8 examples reasonably well, as extensions of the order 2 weak central groupoid, but unfortunately they do not generate any new anti-implications. It is possible that order 18 examples may do so, however (all known finite examples have order either a square, or twice a square). In this thread in particular, "experimental mathematics" paradigms seem to be particularly promising; analysis of the various examples of weak central groupoids have been very useful in formulating fruitful conjectures and discussion.
- For the other outstanding three-variable law (854), we have a sporadic order 12 magma that has some intriguing properties, but is still somewhat mysterious. Perhaps further examples are needed here.
- For the final outstanding law (1516), a large number of "immunities" for this problem have been collected, as well as some interesting identities that are "near misses" to the target goal 255. Again, having more examples may help.
Vlad Tsyrklevich has made progress on understanding the finite magma version of the implication graph, in particular generating scores of new Austin pairs.
There was some discussion about how easy it is to extend our numbering system to arbitrarily long equations, and whether it is worth refactoring to a different numbering system. There have also been some other technical discussions and pull requests regarding optimizing the code in various ways; among other things, this has kept the "build time" of the entire project to reasonable sizes (15 minutes or so), which is a largely invisible but important achievement to keep the project running smoothly.
Day 29 (Oct 24)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586832 | 13268287 | 238 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 56 |
The lone movement on the dashboard today is Alex Meiburg's formalization of the "Obelix does not imply Asterix" anti-implication, closing out the last remaining open statement from the Asterix "village" of equations. The brave Gauls have finally been conquered!
Looking back at the where the project was in Day 13, in which we had encountered our first truly difficult set of implications in the Asterix "village" but had almost a thousand implications yet to resolve, it is remarkable both how far we have come, and how far we still have to go. Despite the village being immune to all finite magma attacks (and hence to some other attacks, such as linear magma attacks), they all fell relatively easily to either a pure greedy approach or a translation-invariant greedy approach. These approaches, which were invented specifically to handle this village, were then responsible for the bulk of the subsequent progress, though we also still had significant advances coming from other techniques such as ATP-powered finite magma search, noncommutative linear constructions, and extensions from simple base models.
But the five remaining equations are extremely resilient. They are all known to have a large number of "immunities" and "resistances"; in particular, the three remaining two-variable laws (1323, 1516, and "Ramanujan" 1729) are known to be immune to (both commutative and noncommutative) translation-invariant or linear constructions, as well as finite constructions; among other things this also rules out an otherwise general looking "polynomial in residue classes" (PORC) approach, at least in the commutative setting. We still have some ideas here, such as extending a (moderately large) base model via some modified greedy approach, perhaps with heavy ATP assistance, but they are putting up a fierce fight.
The two three-variable equations, the weak central groupoid law 1485 and 854 have fewer immunities - in particular, either could still fall to a well-chosen finite counterexample as far as we know - but, despite a lot of progress in understanding these equations, we have not ruled out any anti-implications on either for a few days. With weak central groupoids, we now have a reasonable number of new finite examples of order 8 and 16, but all of our examples are either central groupoids (whose order is a square), or an extension of an order 2 magma whose order is twice a square, and we now know that these types of examples cannot resolve any new anti-implications. With 854, the equation is surprisingly "mutable", and we can generate a quite large number of examples by taking one multiplication table obeying the law and adjoining an additional element, but it seems that this technique needs to be iterated quite a few times before it actually generates a counterexample to the laws we want. I feel of the five outstanding equations, this is the one where we are closest to solving the problem just by pursuing the iteration idea, but it is still work in progress.
On a lighter note, we have some discussion on what "favicon" would be best for an visualization feature Eric Taucher is proposing. Feel free to weigh in with your suggestions! We may soon put it to a vote.
Day 30 (Oct 25)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586832 | 13268287 | 238 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 56 |
Perhaps the quietest day of the project so far. No movement on the dashboard unfortunately; the proofs remaining to formalize are somewhat lengthy, and the five outstanding equations are proving extremely stubborn. Greedy algorithm constructions have helped a little bit with the study of weak central groupoids, leading to several new constructions and a relaxation of the constraints needed to generate counterexamples, but no actual counterexamples have been found so far, and ATP searches are indicating that they are quite rare. For the strangely mutable equation 854, Douglas McNeil has been steadily building examples of magmas with increasingly many violations of equation 10, a precursor to the actual equations we wish to refute, so hopefully we will see a breakthrough there soon.
Day 31 (Oct 26)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586832 | 13268287 | 238 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 68 | 146 | 24 |
A major breakthrough on the largest source of open implications, the weak central groupoid law 1485, which had 19 open implications. Thanks to the concerted efforts of the 1485 team (including key contributions in the last few days from Andy Jiang, Matthew Bolan, Kevin M, Mario Carneiro, Michael Bucko, Pace Nielsen, and others), only three of these implications now remain open; with duality, this settled 32 of the 56 outstanding implications, giving a very pleasing completion rate of 99.9999% (six "nines" of purity).
The route to this progress, which unfolded over a period of ten days, was rather complicated. The classic paper of Knuth on central groupoids already identified an important graph-theoretic interpretation of such groupoids. Nine days ago, we had worked out the analogous graph-theoretic interpretation of weak central groupoids, but did not know what to do with it at the time. After a few days of mostly negative progress (ruling out some possible attacks on the problem), Kevin M and thormikkel proposed systematically searching for small finite magmas. After a lot of mostly computational effort by many contributors (including Kevin, thormikkel, Jose Brox, Ian Duleba, Daniel Weber, Bernhard Reinke, and Pace Nielsen), a picture gradually emerged in which some new weak central groupoids could be constructed as "extensions" of a simple order 2 weak central groupoid. Sadly, all such extensions could then be checked to obey all 19 outstanding implications, so were not directly useful for counterexamples. However, as proposed by Pace, a greedy construction on some larger base than a 2-element base might work. As a proof of concept, Matthew Bolan and I were able to construct infinite (strong) central groupoids with a translation invariant model, and Andy Jiang contributed a nice representation theoretic argument - related by the way to a matrix argument in Knuth's paper - that showed that such objects could not be constructed in for finite magmas. This gave increased confidence that the greedy extension approach on an infinite carrier was the most promising way forward, though further ATP-assisted calculations from Pace Nielsen, David Weber and Zoltan Kocsis indicated that the translation-invariant hypothesis was creating obstructions and would likely have to be abandoned. At this point I proposed relaxing the requirements on the base to try to get larger classes of weak central groupoids for counterexamples. The new construction required the discovery of some suitable finite "relaxed weak central groupoids", but very quickly Michael Bucko and Andy Jiang produced such examples, which after some iteration were able to first refute 1483, and then finally fifteen other implications as well. The final three outstanding implications (to the single-variable equations 151, 3456, and 3862) look quite challenging (Pace observed that these are completely immune to translation-invariant approaches, for instance), but hopefully this new method can also resolve these final implications as well. Already, Matthew Bolan worked out that these three implications are logically equivalent to each other.
Hopefully the above description demonstrates that this was truly a team effort, with an extremely fluid flow of mathematical progress coming from interactions between many participants, very much in the style of the older "Polymath" collaborations, but now with significantly more computer assistance (and also Lean formalization of some key steps already thanks to the quick work of Mario Carneiro, although the full formalization of the above arguments will likely take a bit more time). In fact the summary I provided above only covers about half of the discussion on this problem; there were many other contributions as well pursuing other directions, which may not have directly led to the final breakthrough, but which definitely helped shape both the "positive space" and "negative space" of results and obstructions around this problem that helped us get on a promising track eventually. Apologies to anyone whose name I neglected to mention above!
Besides this progress on the primary goal of the project, there are some efforts (by Eric Taucher, Adam Topaz, Michael Bucko and others) to take the data already obtained by the project and try to present then visually in new ways, or to perform machine learning algorithms on them. Some of this may end up being part of the paper we are planning to write on this project, but some may be completely separate spinoffs. I'm very happy to see that people are already starting to take the partial results we already have and do interesting experiments on them that I would not have anticipated.
Day 32 (Oct 27)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586836 | 13268315 | 206 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 24 |
After a heroic effort, Mario Carneiro has formalized all the recent progress on the weak central groupoid problem, making a notable dent in the outstanding count of claims needing to be formally proven. Furthermore, he has done so by establishing an abstract form of the greedy algorithm, which will be a useful contribution for the rest of the project (the majority of the 64 unformalized conjectures are implementations of such an algorithm), and also a nice contribution to Mathlib. The formalization also revealed some inefficiencies in the original argument (two of the axioms I had placed in the writeup of the greedy construction were in fact not necessary), and in general I now have a much better idea of why this particular approach, in which a relaxed version of the desired magma is constructed first, and used to guide the actual version, is so well suited for the weak central groupoid problem, and may not be as effective for other equations such as 854, although we are still trying to locate some candidate relaxed solutions to that equation too, though so far without success.
The remaining six implications relating to 1485, while known to all be equivalent to each other, are proving incredibly stubborn. Not even a relaxed counterexample to such equations can be found among all small multiplication tables, despite substantial computer searchers by multiple contributors, however they are turning up some new facts about weak central groupoids, particularly relating to the properties of squares x◇x, that are intriguing.
Day 33 (Oct 28)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586838 | 13268317 | 202 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 20 |
Another theoretical advance, this time on the mysterious three-variable equation 854. Here we decided to return to syntactic analysis, and discovered that the universal magma for this equation is not as inscrutable as previously believed; among other things, it obeys a handy "unique factorization property" which we could use to disprove two of the five open implications. This was then formalized at lightning speed by Mario Carneiro, leading to the movement on the dashboard today. It's still unclear how to use this technique to attack the remaining three implications of 854, but we have now scored two partial victories against this equation, the first with explicit finite models, and the second with the universal model, so there is hope of further progress to be made here.
Elsewhere in the discussion, we have uncovered an unfortunate "namespace collision" in our project: we have developed a FreeMagma object in our project which is nearly, but not quite, identical to an object of the same name in Mathlib. As a consequence, we cannot import the entirety of Mathlib into our project. There are a number of ways to resolve this technical issue (we will likely either rename our object, or place it in a separate namespace), but it may require a slightly tricky refactor. This appears to be a situation in which some design choices we made early in the project for convenience ended up being sub-optimal in later stages, and also harder to course-correct for now that a large amount of secondary code is built on top of these initial choices. Probably we can still find an acceptable fix for this problem, but we should take note of such issues in our paper to provide guidance to any future projects of this type that are downstream from Mathlib but also require large amounts of custom definitions.
I discovered today that one of the equations in our study, equation 543, is actually somewhat famous: it was the equation that Tarski demonstrated in 1938 captures the operation of subtraction in abelian groups. It makes me wonder if there are other "hidden gems" in our implication graph that we had somehow not detected in our largely automated efforts to complete the graph.
Day 34 (Oct 29)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586838 | 13268317 | 202 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 20 |
A quiet day, with no movement on the dashboard. We understand the syntactic approach to 854 better; unfortunately, it does not seem to actually give any progress on the three remaining implications, despite resolving two others. For the last remaining implication (up to equivalence) for the weak central groupoid equation 1485, we are beginning to explore the free magma with one generator for this law (inspired by the 854 progress), and have discovered an interesting paper of Kundgen, Leander, and Thomassen discussing ways to modify central groupoids that may be useful. And for the Ramanujan-like equation 1323, Bernard Reinke has proposed a somewhat sophisticated piecewise noncommutative linear ansatz that is not immediately ruled out by the many "immunities" that this problem has, and could be the way forward.
Alex Meiburg proposed a variant of the project in which we study implications of laws "up to change of operation". For instance, Tarski's axiom 543, which codifies subtraction in an abelian group, is neither commutative or associative, but it can define an addition law on the same group, which is both commutative and associative. This is a type of relationship that our current project is not well equipped to detect.
Day 35 (Oct 30)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586838 | 13268317 | 202 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 64 | 118 | 20 |
Another slow day. I had convinced myself at one point that the unique factorization property recently discovered for the free 854 magma could "fix" the previously failed greedy algorithm approach; on working out the details the argument fell apart, but it did uncover a previously unnoticed partial ordering on 854 magmas which could be a useful clue. Bernhard Reinke and Pace Nielsen are continuing to probe the piecewise noncommutative linear approach to equations such as 1323, with some highly nontrivial Grobner basis computations showing up. Kevin M has proposed a potential infinite model for weak central groupoids involving a special zero-like element.
Day 36 (Oct 31)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586838 | 13268317 | 202 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 66 | 122 | 14 |
Some significant progress on the theoretical front. The greedy algorithm approach on 854 has been repaired, by adding an additional axiom that rules out the partial ordering discovered previously from becoming non-trivial. Matthew Bolan was then able to use this greedy algorithm to resolve all remaining implications from 854, which is now (pending Lean formalization, which Mario Carneiro is working on with impressive efficiency) should officially "close off" this cluster of implications, although our understanding of the 854 rule is still somewhat incomplete, and this rule remains a fascinating object of study, being an algebraic structure with an alien blend of structure and randomness. In parallel to this, Jose Brox has revived an old construction method of Kisielewicz which could provide a simpler solution to the 854 problems, but also possibly resolve some of the remaining implications as well. And over on the 1485 thread, Andy Jiang made some further analysis on Kevin's proposed infinite model.
Day 37 (Nov 1)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586840 | 13268321 | 196 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 14 |
The dashboard shows a bit of movement. Mario Carneiro has formalized the recent resolution of the 854 cluster of implications; now only four equations (1485, 1516, 1323, and 1729) remain to be analyzed. After some discussion about the remaining unformalized tasks, some minor housekeeping was done to prune the number of explicit conjectures to be formalized slightly, down to 59. Kevin M, Matthew Bolan, Andy Jiang, and Jose Brox are continuing to make progress constructing an infinite model of the weak central groupoid law 1485 that will refute the remaining implications from that equation, in part with ATP assistance; the model is displaying some intriguing symmetries, but remains incomplete.
Day 38 (Nov 2)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 8 |
A significant advance on the dashboard: the weak central groupoid equation, which we had believed to be the "final boss" of this project, has been completely resolved! The painstaking efforts by Kevin M, Matthew Bolan, Andy Jiang, and Jose Brox to construct a specific model for this equation by imposing additional axioms as guided by ATPs, has in fact paid off by producing a weak central groupoid of order 32 that refutes all outstanding implications from this law, and it was promptly entered into the database by Vlad Tsyrklevich. This new example was initially mysterious, but it was quickly illuminated by Bruno Le Floch, who gave an explicit form of the magma law that revealed it to be a fifth power of the order 2 weak central groupoid, "twisted" by an order 5 automorphism. In retrospect one could have settled this particular equation long ago if we had observed it had this ability to twist its magmas if there was such an automorphism present. Amir Livne Bar-On and Andy Jiang then tested this technique on the other outstanding equations, but unfortunately the semigroup of twists appears to be trivial in those cases. Nevertheless, this is a nice pair of new methods to add to our growing list of techniques to analyze equational laws.
Amusingly, our outstanding conjecture count is now so low that the completion percentage on the dashboard has been rounded up to "100.0000%". (In reality, three equations still remain to be analyzed, with a total of eight outstanding implications conjecturally.)
A technical issue has arisen with some of the code we used to formalize syntactically the 4694 equations we have studied. In order to do the computation quickly, we use the native_decide method, which relies on trusting the Lean compiler to perform formal verifications. Ideally for our final Lean-formalized theorem we would like to avoid this method (and use Lean's internal decide method instead, which is slower), but we have not yet settled on the best long-term fix.
Some GUI improvements: Amir Livne Bar-On has implemented a nice additional feature for "Equation Explorer": implications now have a "Show proof" button that can be used to see the chain of Lean statements used to prove that implication. And Vlad Tsyrklevich has implemented a "show neighborhood" feature for "Graphiti" that lets one see all implications within a certain distance in the Hasse diagram from a given set of laws.
Day 39 (Nov 3)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 8 |
No movement on the dashboard today, but we have some ideas on how to attack 1516, and we have a better understanding of the "twisting semigroup" approach that resolves 1485 (and, we now realize, can be retroactively viewed as implementing our previous resoution of 1117).
The technical issue with using native_decide has been largely resolved through a refactoring of the code. Thanks to Mario Carneiro, Joachim Breitner, Pietro Monticone, and Shreyas Srinivas for working tirelessly to resolve the problem! As one of the outcomes of this process, Mario Carneiro has now formalized in Lean a proof that the list of equations we are studying is in fact the complete set of equational laws (up to relabeling) that one could consider, which will help in formalizing our final "end-to-end" theorem in Lean that all implications between equational laws involving at most four operations have been settled.
Harald Husum has created a nice interactive plot of the different equations in the graph, depicting how many (equivalence classes) of other laws they imply, or are implied by, as well as the number of variables in the equation. This shows visually that equations with many variables tend to imply a lot of equations but are in turn implied by relatively few equations, and conversely for equations with few variables.
Day 40 (Nov 4)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 8 |
Another quiet day. Alex Meiburg has proven some basic implications concerning the Bol/Moufang laws, which are not in our initial set of 4694 equations but are in an extended set. Jose Brox, Bernhard Reinke, and others are experimenting with Kisielewicz-type constructions to resolve 1323, but the constructions aren't quite obeying the law in all cases yet. For 1516, we have a difficult possible approach based on completely classifying the free magma, as well as a potentially simpler approach in which we impose some additional axioms, such as requiring cubes to be constant.
Day 41 (Nov 5)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 8 |
Again no movement on the primary dashboard, but a secondary project has been fully resolved (mostly by Vlad Tsyrklevich): the version of the implication graph for finite magmas (as opposed to arbitrary magmas) is (conjecturally) fully complete! This is not in conflict with the above dashboard, because the 8 remaining anti-implications in the original project were known to be "immune" to finite counterexamples (and are thus listed as true implications for the finite magma version of the implication graph). In fact, a couple hundred such implications were found to automatically be of this form (using the fact that on a finite set, surjectivity implies injectivity and vice versa). There were still four outstanding implications that could not be resolved through this approach (or through the existing work on the primary project), but it turns out that there is a cute variant of the "surjectivity is equivalent to injectivity for finite sets" statement that finishes the job there. UPDATE: as it turns out, the finite magma implication graph is not as complete as first thought; hopefully there will be a further update on this in a few days.
We are inching towards few viable strategies to resolve 1516, in particular we may have a candidate for an (over-complete) rewriting system for this equation. And Matthew Bolan has computed the twisting monoid for all 4694 equations, thus finding all possible implications that could have been refuted by the method (unfortunately this list does not include any of the currently unformalized implications).
Our regular weekly updates to the latest version of Mathlib has generated some breakages in our project. Pietro Monticone and Shreyas Srinivas are currently working to fix the problems. We are considering reducing the frequency of the Mathlib updates to reduce the amount of maintainance needed to deal with these sorts of issues. UPDATE: It appears that all the breakages have now been fixed.
Harald Husum produced a variant of his previous interactive image of the implication graph, now colored by the size of the smallest known finite magma (if it exists). This illustrated that most equations have an order 2 model, and the few that do not, imply very few other equations.
Note: starting from this date, updates will become less frequent.
Day 43 (Nov 7)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 59 | 123 | 8 |
Again, no movement on the dashboard the last two days, but work is ongoing in many different directions. We are slowly learning how to use ATPs to help explore various strategies. For 1323, Jose Brox and Bernhard Reinke have been experimenting to adding various additional laws to try to simplify the structure of the magma, without accidentally proving the law we want to disprove, with ATPs helping to rapidly rule out suggestions that won't work. Kevin M, Pace Nielsen and myself have been doing similar things over at 1516, though with a rather different approaches (trying to add as few additional rules as possible to close the argument, rather than as many); my approach for 1516 was becoming too complex (it has quite a lot of "sporadic" consequences, particularly regarding squares and cubes), but following a suggestion from Andy Jiang, I have proposed a simpler version of it for 1323. Amir Livne Bar-On also has clarified an interesting order 8 model for 1516, while Ibrahim Tencer introduced a modified abelian ansatz for 1323, while Jose Brox and Bruno Le Floch analyzed a piecewise linear ansatz for the same equation.
Alex Meiburg and Bruno Le Floch have been studying laws that are in some sense "definably equivalent" to a law for groups or abelian groups. Even pinning down what "definably equivalent" means is non-trivial, but things are gradually getting clearer.
The many recent issues related to Mathlib updates has triggered an extensive discussion on how frequently we should keep updating to Mathlib, and more generally what the relationship with Mathlib should be going forward. We don't exactly have a consensus on these questions yet, but it is healthy to have these discussions, and hopefully we can converge to a sustainable solution.
Day 45 (Nov 9)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 61 | 125 | 4 |
It's been a while, but finally there is movement on the dashboard! Of the three equations left to attack: "Ramanujan" 1729, the "Mirror Ramanujan" 1323, and an additional equation 1516 - we finally have resolved the implication to 1323, with a solution that also resolved one of the implications from 1729, leaving only two implications and their duals to settle!
This was another team effort where progress (of both "positive" and "negative" types) was slowly made over the last two weeks or so. Some initial ansatze proposed by Bernhard Reinke and Amir Livne Bar-On did not seem to make much positive headway, but led Sebastian Flor to discove that the problem could not be solved if squaring was constant (in fact, the implication collapsed to the Putnam implications!). Gradually, we realized that one should limit the range of the squaring operator to some moderately large portion of the magma, rather than try to squash it down to just one or two values, though we knew that we could not make squaring surjective. Various modified linear or Kisielewicz type models, or a modified free model were proposed, as it turned out the ultimately successful approach came from Jose Brox's insight to study unital models (with a multiplicative identity), in which case the law split into two simpler laws, one involving left and right multiplication by squares, and the other involving left and right multiplication by arbitrary elements. This was fleshed out with several ATP-assisted explorations, as well as Bernard Reinke's suggestion to also impose that squares commute, an idea that was refined further by Jose Brox. Ibrahim Tencer then proposed another modified linear model that was compatible with these assumptions. Meanwhile, I was clinging on for far too long to a modified free magma approach, but I finally found a counterexample blocking that approach from working without major modification, so I paid more attention to the other parallel efforts, including Bruno Le Floch's suggestion to build the magma on the squares first and then on the non-squares. In the end, a slight modification of Bruno's method (making the set of squares infinite instead of finite) allowed a now-standard greedy algorithm approach to work!
Elsewhere, more clarity has been achieved on the finite magma variant of the project by Vlad Tsyrklevich; we actually have about 30 unresolved implications up to duality and some conjectures, including ones which actually have been proven in Lean+Duper, but not integrated into the main Lean codebase as we are refraining from installing Duper there.
Bernhard Reinke and Pace Nielsen are starting to tackle the pile of conjectures that were coming from the translation-invariant greedy method, so hopefully we will get some dashboard movement there soon.
Day 47 (Nov 11)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 62 | 126 | 2 |
More progress on the dashboard: the "squares first!" method that resolved 1323, also resolved 1516! The general strategy here was to first figure out what the multiplication table should look like when multiplying square elements with themselves, then square elements with non-square elements, then finally non-squares with arbitrary elements, as the structure of the equation meant that one could mostly work out each question in this sequence without much regard for later ones in the sequence so long as certain compatibility conditions were satisfied. The simplest model would have been if there was only one square, but we had long known that to be impossible; and Matthew Bolan used an ATP to also rule out having just two squares (though later, as nicely summarized by Jose Brox, we realized that that different ATPs had different strengths and weaknesses for questions like these, and one had to interpret negative results from an ATP with care). Eventually we found a theoretical explanation for why in fact no model with only finitely many squares would work, and this inspired the final solution (and, after prompting by Andy Jiang, I recorded the thought process leading to it). A key ingredient needed was to first build a model of the 1516 equation on the squares which had a needed "double right surjectivity" property, which most of the known models failed to have - but fortunately, Pace Nielsen had previously built a greedy translation invariant model for exactly this equation which did the trick with only minor modifications!
Matthew Bolan, Daniel Weber, and others have made progress on three equations (representing 20 implications) that we had previously resolved using a greedy approach powered by large SAT solver calculations, which made them unsuitable for formalizing in our current version of Lean. By introducing a new technique of imposing constraints in the greedy algorithm, such as ruling out idempotents or forcing a homomorphism to a given reference magma, many of the rules in the greedy ruleset could be eliminated. In one of the three equations, the proof is now SAT-solver free and suitable (in principle) for translation into Lean; the other two are still being worked on. It is also possible that similar techniques could handle other outstanding unformalized equations, in particular 1076 which is responsible for 80 of the 190 outstanding implications.
Shreyas Srinivas gave a preliminary update on the last remaining unresolved equation, the "Ramanujan" equation 1729. Thus far the results have mostly reported negative progress, but this follows a similar trajectory in other equations in which a number of initially promising approaches are gradually ruled out one by one until the eventually successful method is finally brought into view.
Day 49 (Nov 13)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 62 | 126 | 2 |
The dashboard is again static, but a lot of progress behind the scenes. We now have an approach to resolve the last remaining implication (1729=>255) and its dual, based on the "squares first!" method that also was behind the previous two resolutions; one needs a suitable base model on the squares to get started, but Shreyas Srinivas has some ideas on using some stateful heuristic-inspired constructions to do this. For the remaining outstanding implications, we have found proofs of most of them that avoid the translation-invariant greedy approach and are closer to the "vanilla greedy" method that is already automated; this will hopefully allow for many of the unformalized resolutions to be resolved in a semi-automated fashion.
The finite magma (or "Austin pair") variant of the project is becoming more tightly integrated into the main project. Vlad Tsyrklevich has implemented support for the finite implications into Equation Explorer and Graphiti; the status of the finite implication graph is perhaps a couple weeks behind that of the classic implication graph, but the gap does not seem insurmountable. Vlad has also started systematically investigating "Austin laws of order 5": laws that are trivial for finite magmas, but non-trivial for infinite magmas, aided by a new script by Bruno Le Floch to quickly look up the equation id of any reasonable length equation.
Alex Meiburg, Bruno Le Floch, and others are discussing ways in which operations obeying one law can define (slightly different) operations obeying another law, for instance an operation obeying a law for addition in an abelian group could define a law for subtraction. It seems that one might be able to get definitive answers here for laws defining well known operations, such as multiplication or division in a non-abelian group.
Day 51 (Nov 15)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586845 | 13268322 | 190 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 62 | 126 | 2 |
No explicit movement on the dashboard, but two implications (and their duals) are very close to being formalized, and the final (again up to duality) unresolved implication mainly just needs a suitable base model to start the "squares first" argument. So I expect movement on these fronts. Bernhard Reinke also uncovered an issue with a recently (informally) established refutation I had written, but a patch has been implemented.
Bruno le Floch and Jose Brox have been investigating a spinoff question, which is to locate all the order 8 "Higman-Neumann laws": laws that characterize division in a non-abelian group. It is known that any such law must have order at least 8, and Higman and Neumann produced a single such example of an order 8 law, but it appears that there are some additional equivalent laws of equal length. One consequence of these sorts of investigations is that we are learning more about the strengths and weaknesses of different ATPs.
The finite magma graph had 26 outstanding implications (after reducing by conjectures and duality); five of them have now been resolved. Steady progress is also being made by multiple contributors on determining all the laws of order 5 that only have trivial models.
Eric Taucher has made a prototype "Finite Magma game" in which one can attempt to fill in a magma in a "Sudoku" style to obey various axioms. It is still in very early stages of development, but this could be a very nice outreach tool to popularize the project in the long term.
Day 53 (Nov 17)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586846 | 13268323 | 188 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 61 | 125 | 2 |
A little bit of movement on the dashboard; Bernhard Reinke has formalized one of the translation-invariant greedy constructions, and is now looking to adapt that formalization to some other currently unformalized refutations.
There was a scare with the 1323 construction, when Bruno Le Floch pointed out an important typo in the blueprint argument for this equation; fortunately it was possible to patch this argument, though at the cost of making it more inelegant. On the other hand, this also uncovered a problem with adapting this construction to the outstanding implication 1729->817: it turns out that all such constructions also automatically obey 817! Presumably this can again be fixed by making the model more complicated, but it is still an annoying obstacle for the final unresolved implication.
In the search to classify all order 8 Higman-Neumann axioms for group division, Bruno Le Floch, Jose Brox, and Vlad Tsyrklevich have determined the list up to about 80 potential candidates. Interestingly, some of them can be proven to be group division axioms for finite magmas, but there is a chance that a greedy construction can show at least some of them are not of this type in the infinite case.
Day 55 (Nov 19)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586854 | 13268337 | 166 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 51 | 113 | 2 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10736 | 8167997 | 586201 | 13268288 | 414 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 25 | 339 | 4 | 6 | 40 |
As you can see, Vlad Tsyrklevich has added the statistics for the finite magma implications to the dashboard. The statistics are close to the infinite magma implication graph, but with a few more positive implications (including several that require formalization), and fewer refutations, in particular most of the refutations based on greedy constructions are unavailable in the finite case. Progress there is lagging behind the primary project, but some progress is being made. For instance, recently we obtained some new finite refutations for implications that had previously been refuted by an automated, but infinitary, greedy approach, which is why the finite conjecture dashboard contains both explicitly true and explicitly false statements. The finite counterexample can be verified by computer, but is a little too large to fit into the Lean codebase without slowing the compilation time down noticeably, so we are currently working to shrink its size (initially it was of size 84, but Douglas McNeal has managed to get it down to size 50, which is nearly within range of reasonable Lean compilation).
One byproduct of this analysis is that we have finally have at least a partial explanation for the mysterious "twinning" phenomenon of two equations, 503 and 476, that had been observed a month ago: for finite magmas at least, there is a simple way to transform a 503 magma to a 476 magma and vice versa.
Bernhard Reinke has been making steady progress in formalizing the translation-invariant greedy constructions, although an obstacle has arisen in that some of the constructions of initial seeds contained typos. However, some refutations could be salvaged, and we are close to finding replacement seeds (albeit at the cost of abandoning the translation invariant approach, as the remaining problematic implications are now known to be immune to translation-invariant models).
Jose Brox and Bruno Le Floch continue to whittle away at the candidate Higman-Neumann laws of order 8; there are now about 40 candidate laws whose status is not fully resolved.
The last remaining implication needed to complete the primary project, 1729->817, remains challenging, but Shreyas Srinivas did report whether certain simplifying axioms could safely be added to the problem (unfortunately, it appears that many such axioms automatically imply 817 and so cannot be used).
Frédéric Chapoton has added some commentary to two equations that already appear in the literature: the "NAP law" for non-associative permutative operads, and the "flexible algebra law".
Day 57 (Nov 21)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586856 | 13268339 | 162 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 52 | 110 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10739 | 8168042 | 586201 | 13268288 | 366 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 19 | 297 | 4 | 6 | 40 |
A key milestone today: the last of the unresolved implications from the main project, 1729 -> 817, has now (pending verification) been resolved. In the end, a rather complicated version of the "squares first" strategy did work, after building the rest of the multiplication table in the right order (it seems the thing to do is to first build the "non-squares x squares" portion of the table, then reduce the "squares x non-squares" portion to the "0 x non-squares" row, and build that row concurrently with the "non-squares x non-squares" portion by a complex greedy algorithm. There may be simpler approaches to resolve this implication, and we will continue looking for such as the current argument may be challenging to formalize, but this particular implication is known to have a large number of "immunities" which suggests that any construction cannot be overly simple.
With this milestone, we have just opened up a discussion on how to write the paper; thanks to previous planning, a draft skeleton is already in place, but there will be a lot of work needed to update it and convert it into a submittable form.
Formalization of previous arguments (by Bernhard Reinke and Amir Livne Bar-on on the original project, and Vlad Tsyrklevich for the finite magma project) continues at a steady pace, and Matthew Bolan has also been filling in some of the sketchier human-written greedy arguments by supplying proper seeds (the lack of which had temporarily created gaps in some of our claimed proofs). Many of the outstanding arguments share features in common, and hopefully we can leverage that to formalize them in bulk more efficiently than if we had to write a custom argument for each implication.
Jose Brox and Vlad Tsyrklevich have also made progress in classifying which of the order 5 equations have only trivial models, in both the finite magma and arbitrary magma settings. Interestingly, it appears that for such lengthy laws, the choice of parameters for ATP runs becomes quite decisive in being able to use such tools effectively with reasonable computational costs. Jose Brox also reported some progress in resolving some of the order 8 equations whose equivalence to the Higman-Neumann equation for group division was unknown.
Day 59 (Nov 23)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586856 | 13268339 | 162 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 52 | 110 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10739 | 8168042 | 586202 | 13268289 | 364 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 19 | 297 | 4 | 6 | 38 |
With the primary goal provisionally completed, work is settling down to a more sedate pace. Not much explicit movement on the dashboards, with the lone update coming from Vlad Tsyrklevich discovering another finite counterexample for one of the outstanding implications (and its dual) for the finite magma graph. The draft is beginning to take shape, with a process in place for co-authors to declare their contributions. Some of the informal proofs are being corrected or simplified to assist with the formalization process.
Going forward, I plan to update every three days, rather than every two days.
Day 62 (Nov 26)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586865 | 13268354 | 138 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 45 | 93 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10739 | 8168042 | 586203 | 13268290 | 362 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 19 | 297 | 4 | 6 | 36 |
The pile of unformalized proofs on the main project is steadily shrinking, in large part due to Bernard Reinke's ongoing formalization of the implications proven by both translation-invariant and non-translation-invariant versions of the greedy method. Vlad Tsyrklevich also used Vampire to find a further small magma counterexample that resolved one of the outstanding implications in the finite graph. Some other small observations on other outstanding implications here have been collected by Matthew Bolan and myself, although no major breakthroughs have occurred on this front yet.
Several sections of the paper now exist in draft form, and others have been set up as Github "issues" for contributors to work on, so the writing is proceeding at a good pace, and hopefully will be in a satisfactory state by the time the formalization is completed (maybe by the end of this year?).
There was some discussion as to whether we should try to formally benchmark the ATP performance on our project. The consensus was that as we do not seem to have experts in ATP analysis, we should instead present a more informal "field report" of our observed experiences with ATPs, but leave it as an open problem to see if our project can somehow be used to develop high quality ATP benchmarks.
Eric Taucher continues to add features to a "Finite Magma Game" that will hopefully make the basic concepts of magmas and equational laws accessible at the student level.
The Higman-Neumann spinoff project has located some positive implications (involving laws of order 8) that are true, but take ATPs several minutes to establish. This is in contrast with the original project involving order 4 equations, in which all positive implications take mere seconds (and most take a fraction of a second). This is something that we will likely note in the aforementioned "field report".
Day 64 (Nov 28)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586908 | 13268399 | 50 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 17 | 33 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10741 | 8168048 | 586205 | 13268294 | 348 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 18 | 292 | 4 | 6 | 28 |
Quite a bit of progress on the dashboard the last few days. Bernhard Reinke has continued to formalize many of the greedy constructions, including the ones from Equation 1076 which had been responsible for 80 unformalized implications; Bernhard and Shreyas Srinivas are also working to streamline the code and make it easier to resolve the last few implications that can be handled by this method. Meanwhile, Vlad Tsyrklevich formalized some finite implications, while Matthew Bolan and I found some further finite counterexamples to outstanding implications. The latter has introduced a new "semi-direct product" construction for magmas that has already proven useful for finding further examples: Matthew has just found a counterexample for another equation as of this time of writing. The earlier construction of Matthew for 1486 (a variant of the "weak central groupoid" law that was our "final boss" for many weeks) has led to some interesting further investigations by Matthew, Douglas McNeil, and Bruno LeFloch on the restrictions on the size of finite models of this equation.
The Higman-Neumann project continues to slowly move forward with a few more implications resolved, though it is becoming clearer that having a more integrated suite of automated tooling to analyze magmas would be helpful, as a possible future direction after the primary goals of this project are completed. But it at least has helped give experience in how to use the various theoretical and automated tools.
Day 67 (Dec 1)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586914 | 13268411 | 32 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 11 | 21 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10742 | 8168049 | 586210 | 13268301 | 334 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 17 | 291 | 7 | 9 | 10 |
Quite a bit of progress on the dashboard the last few days. Bernhard Reinke has continued to formalize several of the greedy constructions, and also unify some of the code used in these constructions. On the finite front, Matthew Bolan and Douglas McNeil were able to construct many counterexamples to outstanding implications using the new "magma cohomology" method and an existing "extend and modify existing magmas using ATPs" method respectively, to the point where just two equations remain to be analyzed, 677 and 1518. Vlad Tsyrklevich also formalized one of the outstanding positive implications for the finite graph.
Some very large ATP runs by Jose Brox and Vlad Tsyrklevich have made progress on the other problems we are tracking, namely the order 5 Austin laws and the Higman-Neumann order 8 laws (the latter needing more than 15 minutes for an ATP to resolve!). ATPs were also deployed by Jose on the topic of understanding finite 1486 magmas, although here the results were negative.
Day 70 (Dec 4)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10742 | 8168049 | 586210 | 13268301 | 334 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 17 | 291 | 11 | 13 | 2 |
Some progress on the dashboard. Amir Livne Bar-On formalized an old target refutation (of the "Dupont->Dupond" implication) by the translation-invariant greedy method. I managed to locate a rather large (order 522) counterexample to the outstanding implications from 1518; the counterexample can be easily verified in seconds by ordinary Pythons scripts (and by our finite magma explorer), but is too large to verify in Lean with our current tooling. This has then sparked a lively discussion at the above thread as to whether it is possible to have Lean work efficiently with medium sized random access arrays to perform these sorts of verifications purely inside Lean (as opposed to having Lean call an external verifier that it would then have to trust as an axiom). Separately to this, Mario Carneiro and I are discussing how to abstract the construction and try to verify it from the procedural rules generating the example (which was formed by a rather chaotic ad hoc process of putting together "good cycles" in finite carrier that obeyed certain axioms and avoided collisions) rather than brute force check the entire 522 x 522 table. We also have several other large counterexamples, mostly generated by the cohomology method, that face similar issues, although Matthew Bolan has made some progress in shrinking their size slightly, for instance shrinking an order 169 example to an order 65 example.
There is now only a single equation, 677, for which we do not even conjecturally understand the finite model implication (to 255). So we are close to the milestone of conjecturally completing the project for both the infinite and finite magma implication graphs! Perhaps because the end is in sight, there is now extensive discussion by Mario Carneiro, Vlad Tsyrklevich, Joachim Breitner, Andrés Goens and Alex Meiburg on how to efficiently state and prove the "final theorem" in Lean that would completely verify the entire graph (in a fashion that does not require 22 million separate proofs!).
There has been some discussion by Douglas McNeil, Ibrahim Tencer, and others on the "future directions" thread about possible structural classifications of equational laws, in particular trying to formalize the notion of which laws are "rigid" with few solutions (and strong restrictions on their cardinality), and which ones are "mutable".
The paper remains half-written, but one benefit to having the writing process done through Github is that minor corrections can be pointed out either by co-authors, or by visitors to the project; we have already collected two such corrections. Traditionally, the writing process is a closed affair, with drafts only viewed by a small number of coauthors (and sometimes even individual coauthors, when tasked with writing a section, do not reveal their in-progress work to the other coauthors). It thus requires a certain change of habit (and some self-confidence) to make the writing process more open, but with a large and complex collaboration such as this, it seems to be the best available option.
Day 73 (Dec 7)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10742 | 8168049 | 586214 | 13268309 | 322 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 8 | 300 | 6 | 6 | 2 |
The dashboard (which is now significantly expanded with additional statistics and downloadable links to data, thanks to Vlad Tsyrklevich) has a bit of movement on the finite side: Matthew Bolan and I were able to shrink the large finite counterexamples down to the point where several can now be formalized directly in Lean, and have been shrunk to the size were some of them were able to be formalized as is. The remaining two counterexamples now have order less than or equal to 256, and Kyle Miller has developed a way to use Lean's native base 256 encoding to manipulate arrays of this size, so in principle we should be able to formalize all the remaining refutation conjectures on the finite side. (Also, Matthew has also been able to represent some of these counterexamples as low degree polynomials, leading to an alternate route to formalization through polynomial algebra.) As for the positive implications (which were previously only proved by the combination of Lean and Duper), Amir Livne Bar-On and I now have human proofs of all of these that are relatively short, so there should be no obstacle to formalizing them either.
This leaves the final unresolved implication 677 -> 255. Here we have very few finite models to work with - the smallest non-trivial one is of order 5, and all of them are linear. However, we are beginning to make progress, with many contributions from Ibrahim Tencer, Pace Nielsen, Douglas McNeil, Matthew Bolan, Bruno Le Floch, and Jose Brox; in particular, we have a fairly complete understanding of all the linear models, some negative results ruling out (or making unlikely) some possible constructions, and some emerging clues that right-cancellativity may be a key property to focus on.
Eric Taucher has been working on developing a "Finite Magma Game" to illustrate in a non-technical way how magma laws work, with several demos now live. He is soliciting input for possible improvements, please feel free to contribute suggestions!
We are slowly setting up a workflow for collaboratively working on the paper, with one draft section (written by Andrés Goens) currently on Github as a pull request undergoing review. This very open way of writing papers is new to me, but I think it is worth experimenting with. (So far I have been using my administrator privileges to push changes to the paper directly without review, but I will try to also adhere to the PR framework for any major paper edits going forward.) Pietro Monticone has made some changes to the CI to make this process smoother (in particular removing conflicts with the PDF by having the central repository perform the task of compiling the PDF form of the paper.)
Day 76 (Dec 10)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10746 | 8168337 | 586220 | 13268315 | 18 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 4 | 12 | 0 | 0 | 2 |
We've made a push to formalize the outstanding implications on the finite graph, to the point where progress on formalizing that graph is in fact now slightly ahead of that for the infinite graph. Now that all the counterexamples were of order 256 or less, efficient verification in Lean of both old and new counterexamples became possible (thanks to the efforts of Kyle Miller, Vlad Tsyrklevich, Matthew Bolan, and others); and the positive implications initially found with a combination of Lean and Duper had simple enough proofs that they were not too difficult to formalize. The infinite implications remain a challenge, being essentially four quite complex constructions; but three of them have been claimed by project participants, and the fourth has partial progress.
Progress on the paper also continues, with the most significant addition being a draft section by Andrés Goens on the use of automated theorem provers. The paper also continues to recieve a stream of small corrections and updates from various sources, which I certainly appreciate!
Jose Brox has uncovered some strange bugs in Mace4's isomorphism filter as a result of our heavy use of this tool - perhaps another unintended product of our project. A good reminder that even quite established software tools that are not formally verified can contain bugs!
Andy Jiang, Adam Topaz, and others have initiated an interesting discussion as to whether the newly discovered magma cohomology can be connected to more established cohomological concepts, for instance whether there is a topological interpretation in terms of classifying spaces. The lack of associativity does seem to present real obstacles, though.
Day 79 (Dec 13)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
The last of the positive implications for the finite implication graph have now been formalized by Vlad Tsyrklevich, leaving only the extremely stubborn 677->255 finite implication to resolve there. Bruno Le Floch has provided a helpful summary of the state of knowledge we have: a modest number of finite constructions (including some nonlinear ones), but none that seem to lead to a counterexample to 255, for which we have collected a number of "immunities" ruling out certain approaches. It is tantalizing to be so close to being able to declare victory on the primary goals of the project, but some new mathematical idea seems needed.
There have been some interesting explorations of the magma cohomology construction by Bruno Le Floch, Adam Topaz and Andy Jiang, with a few specific equations (such as central groupoids) appearing to have a much fuller cohomological structure similar to the group cohomology arising from the associative law, with hints of higher structures such as A-infinity categories or homotopy coherence emerging.
On a more whimsical note, Jose Brox and Douglas McNeil set out to find the smallest magma that doesn't obey any of the equations in our list other than the trivial ones. It turns out that such a "maximally disobedient" magma has order three.
Day 82 (Dec 16)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
Not much movement the last few days. A few new approaches to the final implication 677->255 were proposed, but the results have been largely negative (for instance, small translation-invariant models are now largely ruled out), and the possibility is emerging that this may have to remain an open problem at the conclusion of the project.
Going forward, I plan to update every four or five days.
Day 88 (Dec 22)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
I am currently on vacation and will be updating infrequently. In any event, it has been quiet. The implication 677 -> 255 for finite magmas remains stubborn, with a steady accumulation of negative results regarding ways to try to relax or otherwise simplify the problem; for instance, ATP investigations seem to have ruled out any "cheap" constructions based on group word maps, and the finite models that we do have do not seem to have any common properties beyond 677 that could help locate further models.
On the other hand, Jose Brox (following a suggestion of Ibrahim Tencer) initiated a study of which of the 4694 laws have "full spectrum", in the sense that models exist at every finite cardinality. It is a measure of our accumulated tools in this area that in short order, Jose, Douglas McNeil, Bruno Le Floch, and Zoltan Kocsis that this problem was solved completely in less than a day!
Day 93 (Dec 27)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
The holiday season continues with a lull in activity for the project. Regarding the final unresolved implication 677 -> 255 for finite graphs, I was able to finally construct a finite non-right-cancellative model (as quickly confirmed numerically by Matthew Bolan), which is evidence towards the falsity of this implication, but unfortunately it is not structured in a way that directly helps construct a counterexample. There are vague hints that one may need to solve some sort of "coloring problem" to resolve the implication.
Day 100 (Jan 3)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
The holidays are ending, but still not much activity on the project at present. Bruno Le Floch has extended the calculation of laws with full spectrum from order 4 to order 5: 39024 equations have full spectrum and 23552 do not, and there are no unresolved cases - again demonstrating the progress the project has made in understanding equational theories. On the other hand, the final finite implication 677 -> 255 remains stubbornly resistant. I proposed a (somewhat desperate) way to attack this implication by decoupling it into two hopefully simpler conjectures, although already the first of these conjectures was demonstrated to be immune to many of our models.
As the research portion of the project winds down, a bit more attention is being turned to writing up the results. Vlad Tsyrklevich contributed a section on the user interfaces we developed for the project.
Day 108 (Jan 11)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
Still no movement on the dashboard, but we are starting a thread to try to assess where we are at with the last few formalization tasks. Bruno Le Floch has continued to extend his exploration of the full spectrum problem, resolving it for all but a handful of equations of order 6 and 7, in addition to the full resolution of equations of order up to 5 already established. It has also been proposed to study the spectrum of magmas that are either "simple", "directly irreducible", or "subdirectly irreducible", but this is a more subtle problem, and so far only the equations of order up to 2 are understood.
Bruno also detected a (somewhat embarrassing) error in the writeup of how we numbered our equations, but fortunately this did not affect any of the code, only the human-readable documentation.
Daniel Weber and Vlad Tsyrklevich will give a talk on this project next Tuesday as part of the "Lean Together" event.
Jose Brox and Zoltan Kocsis pointed out several existing notions in the universal algebra literature, such as admissibility, representability, specialty, interpretability, term equivalence, and polynomial equivalence, that capture precise variants of some concepts we had been discussing regarding when magmas obeying one equational theory can be constructed out of magmas obeying another theory.
A few more negative results were produced on the final unresolved implication of 677 -> 255 for finite magmas; a construction I proposed was shown by Matthew Bolan to not be possible to complete, and Jose Brox reported that ATPs excluded small order magmas from being counterexamples. It now seems likely that this implication will remain open by the time the other implications are formalized, but perhaps the narrative of being able to resolve all but one of the implications makes for a better story than resolving all of them.
Day 115 (Jan 18)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586915 | 13268412 | 30 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 10 | 20 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
The project continues to be somewhat quiet. Bruno Le Floch has done a detailed study of all laws of order at most 2, in particular determining their simple spectrum. As part of this analysis, the "Putnam laws" (14 and 29) were observed to be closely related to existing concepts from design theory, in particular Steiner triple systems.
As for the stubborn anti-implication 677->255, a few more negative results were collected (ruling out several small magma models, and an explanation as to why the greedy algorithm was unlikely to produce left-invertible models), but not much forward progress.
Going forward, I plan to only update when there has been significant activity.
Day 127 (Jan 30)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586922 | 13268427 | 8 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 3 | 5 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
After a long pause, there is now movement on the dashboard; Aaron Hill has completed a (rather heroic) formalization of the many anti-implications stemming from 1692. The two-page human-written proof of Pace Nielsen ended up expanding out initially to 3407 lines of Lean code, although it is now down to "just" 3037 lines after some additional "golfing" of the proof by Pietro Monticone.
There are now three independent anti-implications remaining to be formalized (stemming from 1323, 1516, and 1729). All three have rather tricky human proofs. There were some significant issues reported with formalizing the 1516 anti-implication: the human-written proof was expressed somewhat indirectly as a complex greedy algorithm, described by first describing an initial incomplete algorithm and then applying successive modifications to it until it worked completely, but without describing that completed algorithm in a single location. This style of writing was close to how the proof was discovered; but it made it rather difficult to formalize. The human-written proof has now been rewritten to make the final algorithm more explicit, and hopefully making the formalization process easier.
Other than that, activity has been somewhat quiet. A few minor corrections and updates have been made to the paper draft, and a few more negative computational results were collected by Jose Brox and Jihoon Hyun on the sole remaining (up to duality) unresolved finite implication 677->255, which looks increasingly likely to be an open problem when the time comes to finalize the paper.
Day 133 (Feb 5)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586923 | 13268428 | 6 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 2 | 4 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
Another implication has now been formalized: Lorenzo Luccioli, Pietro Monticone and Marco Petracci, building on prior work by Bernhard Reinke, have formalized the refutation of 1516->255, leaving only two anti-implications remaining to be formalized for the main project. As mentioned recently, there had been issues with the blueprint containing errors, as well as not being written in an ideal formalization-friendly fashion; however, after a rewriting of the blueprint, the remaining formalization was relatively smooth. There was a small speed bump in that the new version of the blueprint required a tweaking of the older construction of Bernard Reinke of a "base" 1516 magma; but fortunately this construction was written in such a way that only a few lines of Lean needed to be modified in order to achieve this. Also, I have found that suggesting a small change (either to oneself, or to a collaborator) to a proof, and then implementing that change, is significantly easier in a formalized proof than an informal one, due to the extreme precision available in specifying the change, and the near-instant feedback of seeing what parts of an argument break when naively implementing any given such change; this is one aspect of the proof writing process where the formalized approach is already superior to the traditional informal one.
A small amount of progress on the stubbornly open 677->255 finite implication: some equivalent forms of 255 have been worked out by Bruno LeFloch and Matthew Bolan, and verified by an ATP. There are still some ideas proposed and other activity on this implication, but we seem to be missing a key breakthrough to truly make an advance on this implication at present.
A listing of this project has been sent as a pull request to mathbases.org, although it does not appear to have made it to the live version of the database yet.
Day 153 (Feb 25)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586924 | 13268429 | 4 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 1 | 3 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
The formalization of the main project is almost done: Amir Livne Bar-On has formalized the anti-implication 1323 !-> 2744, leaving just one outstanding explicit anti-implication (1729 !-> 817) to be formalized! The proof given in the blueprint was a little tricky to formalize directly - for instance, it used a greedy algorithm in which an infinite number of elements were added at each stage, instead of a finite number - but Amir was able to adapt the argument to push the formalization to the finish line. Similarly to the formalization of 1516 !->255, it was convenient to use carriers based on free non-abelian groups, which seem to be easier for Lean to handle even if they are less intuitive than standard number systems like the integers or rationals.
Matthew Bolan has used computer algebra systems (most notably Singular's non-commutative Groebner basis packages) to try to determine exactly which anti-implications can be established by either commutative or non-commutative linear models. A provisional answer has been given, but unfortunately the exercise seems to have turned up some non-trivial bugs in Singular. In principle it may be possible to verify the output here in Lean, but this may require a future project. In any event, this highlights the potential need for future computation-intensive projects for computer algebra packages to offer a way to output proof certificates in a formal language.
Day 177 (Mar 21)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586924 | 13268429 | 4 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 1 | 3 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
While the dashboard remains unchanged, we have started a push to formalize the last remaining anti-implication 1729 !-> 817, after some refactoring of the blueprint and Lean structure for this complex proof to break it up into about a dozen substeps. Hopefully there will be visible progress on this final step soon. After this, the main remaining primary task of the project will be to finalize the draft paper.
Another small task completed: an outstanding task to code an explicit formula for the number of laws of a given order has now been completed by snburris.
Day 201 (Apr 14)
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10657 | 8167622 | 586925 | 13268432 | 0 |
Of the unproven claims, we conjecturally have
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 0 |
Restricting to finite magmas, the corresponding statistics are
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No proof |
|---|---|---|---|---|
| 10750 | 8168349 | 586220 | 13268315 | 2 |
and
| Explicitly true | Implicitly true | Explicitly false | Implicitly false | No conjecture |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | 2 |
It took a little longer than expected, but the primary goal of the project is now completed - all implications and anti-implications between the initial set of 4694 equational laws have now been formalized in Lean! The final anti-implication, 1729 !=> 817, was extraordinarily complex, eventually requiring a blueprint of nineteen custom definitions, lemmas, and theorems, which were formalized by a team effort including Shreyas Srinivas, Aaron Hill, Bernhard Reinke, myself, and others. While at its heart the construction was a greedy construction similar to that seen in previous anti-implications, the particular greedy construction here was extremely intricate, with a given step in the introduction making over a dozen changes to the "partial solution" which had to be verified to not collide with each other, generating over a hundred non-collision checks. The initial blueprint for this contained several mistakes and gaps which required the definition of "partial solution" to be altered several times, and then the non-collision checks redone; but fortunately, with each such change, Lean could verify a significant number of the previous proofs continued to work under the new definitions. This was perhaps a situation in which the current state of formalization was sufficient to make the completion of the proof faster than if it was done by traditional pen-and-paper methods, because of the burden of redoing a large number of case checks every time the definitions were updated. The proof also required significant input from Mathlib's API on free groups, for instance using the fact that these groups admitted a large number of useful representations that could be used to ensure that various words that arose in the construction did not collide with each other.
The notoriously stubborn 677=>255 implication for finite magmas remains unresolved; the tentative belief is that this implication is false, but we have largely exhausted our ideas on this and will likely leave this as an open question for the final paper.
With this milestone, the project now enters its wrapping up phase. We already have a half-written draft of our results: there are several sections that still need to be contributed, but then it is "just" a matter of polishing and proofreading, then the paper can be submitted and the main phase of the project wound down. (But the Github and Zulip channel will remain open, in case of any further queries, corrections, or spinoff projects.)
Day 231 (May 14)
Updates are now more infrequent, given that the formalization phase of the project is largely complete. In particular I will stop reporting on the dashboard statistics unless they change for one reason or another.
Here are some of the things that have happend since the last update. This project was mentioned in a Quanta article and also cited in an article on human-computer interaction and an article on the Busy Beaver project.
Bruno Le Floch provided some relatively short, human-readable proofs of the implication that E1689 implied E2, which was an implication established by Kisielewicz with an early automated theorem prover. As an experiment, I formalized these proofs using a variety of modern computer tools as assistance, notably Github Copilot, the recently released dependent type matching tool canonical, and the large language models "Claude" and "o4-mini". A further formalization (in the theorem prover Acorn) was also recently provided, independently of the Equational Theories Project.
The writing of the paper (which is now titled "The Equational Theories Project: Advancing Collaborative Mathematical Research At Scale") proceeds somewhat slowly, but steadily; for instance, some new references regarding the number of isomorphism classes of magmas of a given size, or the history of the greedy construction, have now been incorporated. Some small improvements to the commentary for various equations are also being implemented.
After a long delay, we have finally started "bump"ing the version of Lean and Mathlib used in our project to the latest version. It turns out that if one delays this procedure for too long, and the code base is large and complex, then there are a lot of minor (and not-so-minor) "breakages" that then need to be patched. This is a potential issue in the long term when formalization has reached the point where we want to "cite" or otherwise incorporate proofs written in other repositories, with slightly different versions of Lean and Mathlib, into one's current project. At some point, projects such as the Equational Theories Project will no longer be actively maintained, and their proofs, while still correct, will become gradually more incompatible with the latest versions of the core Lean libraries. I started a discussion thread on how close we are as a community to automating the bumping process (which is perhaps the simplest case of the more general autoformalization problem), but we don't yet have a satisfactory long-term solution to this issue.
Bruno Le Floch has revived the topic of mysteriously "twinned" equations that came up at an earlier stage of the project, noting that the linear magma models can be used to at least partially illuminate this phenomenon.