Terence Tao on Nostr: As of yesterday, the Equational Theories Project ...
As of yesterday, the Equational Theories Project https://teorth.github.io/equational_theories/ has (provisionally) attained its aim of resolving all 22028942 implications between the 4694 equational laws of magmas involving at most four multiplication operations. We are not fully done yet - there are 52 resolutions that currently only have a human-readable proof but not a Lean-formalized proof (actually, there are a few that are not even human-readable, but are instead computer-generated by some non-Lean program) - but it should now just be a matter of time before we can declare final success in which the full implication graph is completely formalized in Lean. As such, we are now beginning the process of writing up the results.
The full implication graph is too large to easily visualize, but we have tools to inspect fragments of it at a time: for instance here is a graph of all the laws that are implied by Equation 854, x = x ◇ ((y ◇ z) ◇ (x ◇ z)): https://teorth.github.io/equational_theories/graphiti/?render=true&highlight_red=854&implies=854 . The Equation Explorer tool at https://teorth.github.io/equational_theories/implications/ lists all the equations, their implications, and various commentary on some selected equations.
There are various spinoff projects that are still ongoing, for instance to work out the analogous implication graph when restricted to finite magmas, or to perform data analysis on the graph and see if there are any interesting features. We've also learned a lot of lessons on how to run a large collaborative math research project, which we will report in our paper and which we hope will be useful for future such projects. Additionally, I also hope the implications here could serve as benchmarks for future AI math tools.
The full implication graph is too large to easily visualize, but we have tools to inspect fragments of it at a time: for instance here is a graph of all the laws that are implied by Equation 854, x = x ◇ ((y ◇ z) ◇ (x ◇ z)): https://teorth.github.io/equational_theories/graphiti/?render=true&highlight_red=854&implies=854 . The Equation Explorer tool at https://teorth.github.io/equational_theories/implications/ lists all the equations, their implications, and various commentary on some selected equations.
There are various spinoff projects that are still ongoing, for instance to work out the analogous implication graph when restricted to finite magmas, or to perform data analysis on the graph and see if there are any interesting features. We've also learned a lot of lessons on how to run a large collaborative math research project, which we will report in our paper and which we hope will be useful for future such projects. Additionally, I also hope the implications here could serve as benchmarks for future AI math tools.