• gryn an hour ago

    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

    • davidrjones1977 3 hours ago

      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.

      • gigatexal 4 hours ago

        upvoting this hoping someone can dumb it down for me a bit :sweat_smile:

        • schoen an hour ago

          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.