Terence Tao - Using Claude, ChatGPT to Formalise A Theorem About Magmas in Lean

The theorem is that x=(yx)((xz)z) implies the singleton law x=y. I guess this is from the Equational Theories Project:

The purpose of this project, launched on Sep 25, 2024, is to explore the space of equational theories of magmas, ordered by implication. To begin with we shall focus only on theories of a single equation, and specifically on the 4,694 equational laws involving at most four magma operations, up to symmetry and relabelling (here is the list in Lean and in plain text). This creates 4694*(4694-1) = 22,028,942 implications that need to be proven or disproven, creating both “implications” and “anti-implications”.

The singleton law: This is the strongest law, satisfied only by the trivial magmas: the singleton and empty magmas. Many laws are equivalent to this law; informally, they are so "overdetermined" that they can only be satisfied by trivial magmas. In fact, from our list of 4694 laws, exactly 1495 other laws are equivalent to this one.

The equations were enumerated from https://github.com/teorth/equational_theories/blob/main/scripts/generate_eqs_list.py.

Here is the first video (confirming it is the equational theories project)

Subscribe to Terence Tao.

Yesterday I was listening to this interview Curt Jaimungal did with Yang-Hui He, talking about AI and number theory. He makes some interesting points, including the one that the AI companies don't have nearly enough people providing examples of theorem proving in Lean. The models need more training data if they're ever going to get better. I guess projects like this are helping with that.

 Subscribe to Curt Jaimungal.

I wonder if there's a bigger picture worth looking at.  On the one hand, in Homotopy Type Theory you have a topological model of proofs and equivalence, and on the other hand there are all these hard problems in topology and knot theory. See Daniel Tubbenhauer - How good are (quantum) knot invariants? and this 1996 paper by Steven Vickers entitled Topology via Constructive Logic:

See Lindenbaum–Tarski algebra:

In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentences of the theory (i.e., the quotient, under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T). That is, two sentences are equivalent if the theory T proves that each implies the other. The Lindenbaum–Tarski algebra is thus the quotient algebra obtained by factoring the algebra of formulas by this congruence relation. 

Now maybe I have just got my head spinning up my behind, but it seems to me that there could be a correspondence between the algebras Daniel Tubbenhauer talks about at 32:15 when he describes the Jones Polynomial and the Lindenbaum–Tarski algebras of the theory of magmas/groupoids and that this corresponds to the groupoids upon which Homotopy Type Theory is based, so that there is a connection between knot theory and proof theory?

Here's a talk he gave at Lake Como Toposes conference in 2018 "Grothendieck toposes constructively, via arithmetic universes"

And the follow-up talk by Sina Hazratpour "Fibrations of contexts and fibrations of toposes"

I'm lost in a sea of words, not just a lake!

Subscribe to Università degli Studi dell'Insubria.