A pilot project in universal algebra to explore new ways to collaborate

154 pointsposted 14 hours ago
by anothermathbozo

16 Comments

practal

a few seconds ago

This is a great idea, and full of inspiring ideas for what kind of work flows and features a modern theorem proving system could support.

gryn

11 hours 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

brotchie

7 hours ago

Sounds exactly like Truth Mining in Greg Egan's Diaspora.

srcreigh

6 hours ago

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!

photonthug

5 hours ago

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.

khafra

5 hours ago

> 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

srcreigh

4 hours ago

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.

davidrjones1977

13 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.

photonthug

7 hours ago

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.

mncharity

9 hours ago

> 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?

gigatexal

13 hours ago

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

schoen

11 hours 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.

wiresong

6 hours ago

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!

gigatexal

6 hours ago

> 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.

Certhas

5 hours ago

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.

gigatexal

3 hours ago

Awesome thanks for clarifying