Interesting project for anyone who want to start learning lean and contribute to a project.
The project as described in the article is to produce a graph (Poset) where each node is a law (say the commutativity equation for example) and each edge is either a proof of implication or a proof of a non-implication, since this graph is infinite the project limits the laws considered to up to 4 applications of the binary operator.
The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.
The collaborative aspect of the project is to write a proof for each kind of edge (implication and not_implications) between the 4694 considered nodes.
There's also the advantage that a GitHub CI running lean will be setup to automatically check if the pull requests adding theses edges are right or wrong without the need for a human to do the checking of the proofs in their head.
I really love the extent to which Terry Tao has embraced the promise and potential of proof assistants. So many smart and talented people in that community doing so much amazing work. With folks like these pushing the boundaries, the sky is the limit.
Yes! It’s rare and really encouraging to see an established giant embracing and extending the new and reaching outwards to other communities rather than doubling down on the old ways, gatekeeping, moat-building, and defending their kingdom. It’s an unusual source for hope and gratitude maybe, given the esoteric subject matter, but it also might be the only one I see this week.
I love this! Let’s not take for granted that such simple mathematics problems may not have ever been solved yet. What a time to be alive.
> So, the situation here is somewhat similar to the Busy Beaver Challenge, in that past a certain point of complexity, we would necessarily encounter unsolvable problems
I must be a platonist to squirm about this. There are no unsolvable problems with undecidability or busy beaver numbers. The only thing is some math questions are actually infinitely many problems disguised as a single problem.
The halting problem etc is the opposite of unsolvable, it’s so solvable humanity can never finish solving it. It’s infinitely solvable.
It’s as if we found a magical soup which has a new taste every day forever, and we call it “untasteable”. It’s not untasteable! It’s the tastiest thing ever!
This is an interesting perspective, but sticking with the analogy, the situation may appeal more to the tasters than to the chefs, cookbooks, etc. The vast wilderness of mere facts does have some kind of savage beauty, but compressing that into coherent theory is more satisfying and sometimes useful!
Re: beavers in particular, it was cool to see that effort mentioned in the context of large scale collaborations and amateur+professional cooperation, and reflect on similar episodes in the history of science. Re: vast wilderness, computing and complexity is exactly where you’d expect to see natural-science style catalogues of funny looking phenomena due to the recency. Ahead of stuff like systematized comparative anatomy we gotta fill up the zoos and curio cabinets so the systematizers (who are themselves somewhat less likely to be explorers) have plenty of specimens to work with.
That machine doesn’t encode ZF. It encodes a problem that is independent of ZF. And it’s not impossible to prove that the machine runs forever, you just can’t use ZF to prove that.
Usually when we have something like numbers (objects) and something like addition (an operation) we're accustomed to getting various rules that apply.
For example,
a + b = b + a
Also,
a + (b + c) = (a + b) + c
These work for addition and in fact for many other things we can do with numbers that we care about. But mathematicians also study objects and operations where some of these rules don't apply.
A somewhat famous example is about rotating physical objects in space. In that case, it matters what order you do the rotations in ("turn and flip" doesn't end up the same as "flip and turn"!). So if "a" and "b" referred to rotations in space and "+" referred to doing them one after another, then
a + b ≠ b + a
in some cases.
Universal algebra is about thinking about all of these kinds of rules and how they relate to each other, for any kind of objects and any kinds of operations. So numbers are one kind of object and addition is one kind of operation, but there can be infinitely many kinds of objects and infinitely many kinds of operations, and some will follow certain patterns and others won't.
But in some cases, objects and operations that follow certain patterns (sometimes called "laws") automatically have to follow other patterns.
To take one example, if
a + b = b + a
and
a + (b + c) = (a + b) + c
then it is necessarily also true that
a + b + c = c + b + a
Some of these patterns have been very extensively studied because they recur over and over again, or because they apply to things like numbers (and rotations) that we care about a lot in relation to things we frequently encounter in life (and mathematics and computer science). But other patterns may be obscure and not that well-studied.
If you hypothesize some laws about ways of combining objects, you might ask which other laws are necessarily implied (or necessarily impossible) as a result of those laws. Tao noted that there are actually thousands of simple-to-state laws and so a research project is to figure out the logical status of how all of them relate to all of the others. Which ones require others to be true? Which ones prevent others from being true? Which ones are independent of others, so they might be true or not?
There are some charts about familiar classifications of these structures according to certain laws
but Tao is sort of suggesting that this classification is just getting started, and we can learn a lot more about how structures relate to each other.
I should note that he is limiting this to "equational axioms" which means that he's not considering some of the kinds of rules that are often considered in such studies (those containing constants, not just variables). For example, when dealing with numbers and addition there is a number 0, which doesn't change other numbers when added to it. This fact causes lots and lots of nice theorems about arithmetic to work out. There is similarly a "non-rotation" in rotations which doesn't change the position of objects when you "rotate" them by not moving them. That also causes some of the same theorems that would apply to arithmetic with numbers to apply in that case!
Tao's project is, at least for the time being, not considering rules like "there is an object that doesn't cause a change when applied to other objects" (the "law of identity", which is represented by a downwards blue arrow in that Wikipedia article). These rules are important in mathematics, but I guess it's more complicated to consider how they do or don't relate to one another, so this project will simply ignore them, and only consider laws that can be stated only with variables.
Does that help a bit?
I guess another point is just that it's been very common in mathematics to try to consider things at higher and higher levels of abstraction, in order to find theorems that work for many different situations. For instance, Boolean algebra like in computer logic has objects 0 and 1, and operations OR and AND (and perhaps XOR). It turns out that we can interpret Boolean algebra with XOR and AND as a previously-discovered mathematical structure called a finite field
... whereupon tons of theorems about fields immediately automatically apply to Boolean algebra, even though perhaps those theorems weren't originally conceived of as relating to Boolean logic at all. So part of universal algebra is like "if we prove as much as we can with as few assumptions as possible, we can discover results that will readily apply to lots of new situations in the future". What Tao is proposing to do is a part of that undertaking, again at a super-high level of generality.
Not the original asker, but I just wanted to appreciate this explanation-simple, concise, but still maintaining a one-to-one correspondence with the actual mathematics. Thank you!
A really good question! I've been out of the field for a long time, but it's important to stress the difference between "interactive proof assistants" and "automated theorem provers." The latter consist in various software tools that, given a well-formed logical formula, attempt to automatically derive a proof thereof in a given logic. There are of course well-understood limits to such tools given the foundational results of Gödel, Turing etc in the early 20th century.
On the other hand, interactive proof assistants such as Lean, mentioned in the title article, or Isabelle are really something more like functional programming languages in which a human mathematician can specify and prove a given theorem, relying on the work of other mathematicians as equivalent to a third-party library. Again like with programming languages, the different tools will offer various trade-offs between expressibility and the kinds of guarantees that can be made at compile time about the validity of a proof. It has traditionally been viewed as far too time consuming to actually specify even intermediate mathematics in such tools, but LLMs really change the situation, as Terrance Tao in particular has demonstrated.
I have to wonder whether there's a magma where equation 4 holds while equation 7 (commutativity) doesn't. Off the top of my head, I can't think of one but does that mean there absolutely can't be one, like the depicted graph implies?
Interesting project for anyone who want to start learning lean and contribute to a project.
The project as described in the article is to produce a graph (Poset) where each node is a law (say the commutativity equation for example) and each edge is either a proof of implication or a proof of a non-implication, since this graph is infinite the project limits the laws considered to up to 4 applications of the binary operator.
The main goal is not the proofs themselves but experimenting in doing math in a matter that's more similar to software engineering in the open source community.
The collaborative aspect of the project is to write a proof for each kind of edge (implication and not_implications) between the 4694 considered nodes.
There's also the advantage that a GitHub CI running lean will be setup to automatically check if the pull requests adding theses edges are right or wrong without the need for a human to do the checking of the proofs in their head.
partial visualization of the (WIP) graph: https://github.com/teorth/equational_theories/blob/0e67dad3b...
outline of the project: https://teorth.github.io/equational_theories/blueprint/
github repo: https://github.com/teorth/equational_theories
Sounds exactly like Truth Mining in Greg Egan's Diaspora.
I really love the extent to which Terry Tao has embraced the promise and potential of proof assistants. So many smart and talented people in that community doing so much amazing work. With folks like these pushing the boundaries, the sky is the limit.
Yes! It’s rare and really encouraging to see an established giant embracing and extending the new and reaching outwards to other communities rather than doubling down on the old ways, gatekeeping, moat-building, and defending their kingdom. It’s an unusual source for hope and gratitude maybe, given the esoteric subject matter, but it also might be the only one I see this week.
It’s only those with something to prove who do that. He has nothing left to prove. Probably never did; he just genuinely enjoys what he does.
Another fields medalist is also on the case: Tim Gowers
https://gowers.wordpress.com/2022/04/28/announcing-an-automa...
I love this! Let’s not take for granted that such simple mathematics problems may not have ever been solved yet. What a time to be alive.
> So, the situation here is somewhat similar to the Busy Beaver Challenge, in that past a certain point of complexity, we would necessarily encounter unsolvable problems
I must be a platonist to squirm about this. There are no unsolvable problems with undecidability or busy beaver numbers. The only thing is some math questions are actually infinitely many problems disguised as a single problem.
The halting problem etc is the opposite of unsolvable, it’s so solvable humanity can never finish solving it. It’s infinitely solvable.
It’s as if we found a magical soup which has a new taste every day forever, and we call it “untasteable”. It’s not untasteable! It’s the tastiest thing ever!
This is an interesting perspective, but sticking with the analogy, the situation may appeal more to the tasters than to the chefs, cookbooks, etc. The vast wilderness of mere facts does have some kind of savage beauty, but compressing that into coherent theory is more satisfying and sometimes useful!
Re: beavers in particular, it was cool to see that effort mentioned in the context of large scale collaborations and amateur+professional cooperation, and reflect on similar episodes in the history of science. Re: vast wilderness, computing and complexity is exactly where you’d expect to see natural-science style catalogues of funny looking phenomena due to the recency. Ahead of stuff like systematized comparative anatomy we gotta fill up the zoos and curio cabinets so the systematizers (who are themselves somewhat less likely to be explorers) have plenty of specimens to work with.
> There are no unsolvable problems with undecidability or busy beaver numbers.
Actually, if you encode the axioms of ZF into a TM, it's impossible to prove the machine will ever halt:
https://scottaaronson.blog/?p=2725
That machine doesn’t encode ZF. It encodes a problem that is independent of ZF. And it’s not impossible to prove that the machine runs forever, you just can’t use ZF to prove that.
> presents the partially known poset in a visually appealing way
Perhaps a hopefully-compressible correlation matrix, sorted and collapsed on similarity, with mouseover to get equations?
upvoting this hoping someone can dumb it down for me a bit :sweat_smile:
Usually when we have something like numbers (objects) and something like addition (an operation) we're accustomed to getting various rules that apply.
For example,
a + b = b + a
Also,
a + (b + c) = (a + b) + c
These work for addition and in fact for many other things we can do with numbers that we care about. But mathematicians also study objects and operations where some of these rules don't apply.
A somewhat famous example is about rotating physical objects in space. In that case, it matters what order you do the rotations in ("turn and flip" doesn't end up the same as "flip and turn"!). So if "a" and "b" referred to rotations in space and "+" referred to doing them one after another, then
a + b ≠ b + a
in some cases.
Universal algebra is about thinking about all of these kinds of rules and how they relate to each other, for any kind of objects and any kinds of operations. So numbers are one kind of object and addition is one kind of operation, but there can be infinitely many kinds of objects and infinitely many kinds of operations, and some will follow certain patterns and others won't.
But in some cases, objects and operations that follow certain patterns (sometimes called "laws") automatically have to follow other patterns.
To take one example, if
a + b = b + a
and
a + (b + c) = (a + b) + c
then it is necessarily also true that
a + b + c = c + b + a
Some of these patterns have been very extensively studied because they recur over and over again, or because they apply to things like numbers (and rotations) that we care about a lot in relation to things we frequently encounter in life (and mathematics and computer science). But other patterns may be obscure and not that well-studied.
If you hypothesize some laws about ways of combining objects, you might ask which other laws are necessarily implied (or necessarily impossible) as a result of those laws. Tao noted that there are actually thousands of simple-to-state laws and so a research project is to figure out the logical status of how all of them relate to all of the others. Which ones require others to be true? Which ones prevent others from being true? Which ones are independent of others, so they might be true or not?
There are some charts about familiar classifications of these structures according to certain laws
https://en.wikipedia.org/wiki/Magma_(algebra)#Types_of_magma
but Tao is sort of suggesting that this classification is just getting started, and we can learn a lot more about how structures relate to each other.
I should note that he is limiting this to "equational axioms" which means that he's not considering some of the kinds of rules that are often considered in such studies (those containing constants, not just variables). For example, when dealing with numbers and addition there is a number 0, which doesn't change other numbers when added to it. This fact causes lots and lots of nice theorems about arithmetic to work out. There is similarly a "non-rotation" in rotations which doesn't change the position of objects when you "rotate" them by not moving them. That also causes some of the same theorems that would apply to arithmetic with numbers to apply in that case!
Tao's project is, at least for the time being, not considering rules like "there is an object that doesn't cause a change when applied to other objects" (the "law of identity", which is represented by a downwards blue arrow in that Wikipedia article). These rules are important in mathematics, but I guess it's more complicated to consider how they do or don't relate to one another, so this project will simply ignore them, and only consider laws that can be stated only with variables.
Does that help a bit?
I guess another point is just that it's been very common in mathematics to try to consider things at higher and higher levels of abstraction, in order to find theorems that work for many different situations. For instance, Boolean algebra like in computer logic has objects 0 and 1, and operations OR and AND (and perhaps XOR). It turns out that we can interpret Boolean algebra with XOR and AND as a previously-discovered mathematical structure called a finite field
https://en.wikipedia.org/wiki/Boolean_algebra#Values
... whereupon tons of theorems about fields immediately automatically apply to Boolean algebra, even though perhaps those theorems weren't originally conceived of as relating to Boolean logic at all. So part of universal algebra is like "if we prove as much as we can with as few assumptions as possible, we can discover results that will readily apply to lots of new situations in the future". What Tao is proposing to do is a part of that undertaking, again at a super-high level of generality.
Not the original asker, but I just wanted to appreciate this explanation-simple, concise, but still maintaining a one-to-one correspondence with the actual mathematics. Thank you!
> Does that help a bit?
Holy smokes thank you!!! Yeah that makes much more sense now. Thank you for taking the time to write all that up!
Would Godel’s incompleteness theorem throw a monkey wrench into some of this effort? Probably not Tao would have already thought of that I guess.
There is no a priori reason why the aimed for results should be unprovable ala Gödel.
However, it turns out it has been proven that it is. Tao says so in the post:
> I will remark that the general question of determining whether one set of equational axioms determines another is undecidable.
Even though the general problem is undecidable, individual instances are still potentially solvable.
I remark that it's the "several equations -> several equations" that's undecidable
this project focuses only on "1 eq -> 1 eq", so it's even more of a gray area
Awesome thanks for clarifying
A really good question! I've been out of the field for a long time, but it's important to stress the difference between "interactive proof assistants" and "automated theorem provers." The latter consist in various software tools that, given a well-formed logical formula, attempt to automatically derive a proof thereof in a given logic. There are of course well-understood limits to such tools given the foundational results of Gödel, Turing etc in the early 20th century.
On the other hand, interactive proof assistants such as Lean, mentioned in the title article, or Isabelle are really something more like functional programming languages in which a human mathematician can specify and prove a given theorem, relying on the work of other mathematicians as equivalent to a third-party library. Again like with programming languages, the different tools will offer various trade-offs between expressibility and the kinds of guarantees that can be made at compile time about the validity of a proof. It has traditionally been viewed as far too time consuming to actually specify even intermediate mathematics in such tools, but LLMs really change the situation, as Terrance Tao in particular has demonstrated.
For anyone interested in the topic, I highly recommend the work of the CMU logician Jeremy Avigad. See, for example: * Formally Verified Mathematics- https://www.andrew.cmu.edu/user/avigad/Papers/cacm.pdf * Automated Reasoning in Mathematics- https://link.springer.com/chapter/10.1007/978-3-031-63498-7_... * The Mechanization of Mathematics- https://www.ams.org/journals/notices/201806/rnoti-p681.pdf
This is a great post, and full of inspiring ideas for what kind of work flows and features a modern theorem proving system could support.
I have to wonder whether there's a magma where equation 4 holds while equation 7 (commutativity) doesn't. Off the top of my head, I can't think of one but does that mean there absolutely can't be one, like the depicted graph implies?
you mean the opposite way?
article gives proof why 4 implies 7 (thus magma with eq4 always agrees with eq7)