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