Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

BusyBeaver(6) Is Quite Large

scottaaronson.blog

Post reply on HN
Print view View original

61–70 of 232 posts

Re: BusyBeaver(6) Is Quite Large

#61

Post by Xcelerate »

azan_ wrote: post #52
Xcelerate wrote: post #40

Earlier quoted context omitted.

It boggles my mind that we ever thought a small amount of text that fits comfortably on a napkin (the axioms of ZFC) would ever be “good enough” to capture the arithmetic truths or approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity. That the behavior of a six state Turing machine might be unpredictable via a few lines of text does not surprise me in the slightest. A…

> As soon as Gödel published his first incompleteness theorem, I would have thought the entire field of mathematics would have gone full throttle on trying to find more axioms. But why? Gödel's theorem does not depend on number of axioms but on them being recursively enumerable.

Right, Hilbert’s goal was (loosely speaking) to “find a finitely describable formal system” sufficient to “capture all truths”. When Gödel showed that can’t be done, that shouldn’t imply we just stop with the best theory we have so far and call it a day—it means there are an infinite number of more powerful theories (with necessarily longer minimal descriptions) waiting to be discovered.

In fact, both Gödel and Turing worked on this problem quite a bit. Gödel thought we might be able to find some sort of “meta-principle” that could guide us toward discovering an ever increasing hierarchy of more powerful axioms, and Turing’s work on ordinal progressions followed exactly this line of thinking as well. Feferman’s completeness theorem even showed that all arithmetical truths could be discovered via an infinite process. (Now of course this process is not finitely axiomatizable, but one can certainly extract some useful finite axioms out of it — the strength of PA after all is equivalent to the recursive iteration up to ε_0 of ‘Q_{n+1} = Q_n + Q_n is consistent’ where Q_0 is Robinson arithmetic).

Re: BusyBeaver(6) Is Quite Large

#62

Post by nyrikki »

ChadNauseam wrote: post #11
Scarblac wrote: post #4

It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.

The number itself is not independent of ZFC. (Every integer can be expressed in ZFC.) What's independent of ZFC is the process of computing BB(748).

To try and help people digging into this, the following helped me.

Two lenses for trying to understand this are potentially Chastain's limits on output of a lisp program being more complex than the program itself [1] or Markov's proof that you can't classify manifolds in d>= 4.

If you try the latter and need/want to figure out how the Russian school is so different this is helpful [2]

IMHO the former gives an intuition why, and the latter explains why IMHO.

In ZFC, C actually ends up implying PEM, which is why using constructionism as a form of reverse math helped it click for me .

This is because in the presence of excluded middle, every sequentially complete metric space is a complete space, and we tend to care about useful things, but for me just how huge the search space grows was hidden due to the typical (and useful) a priori assumption of PEM.

If you have a (in my view) dislike for the constrictive approach or don't want/have to invest in learning an obscure school of it, This recent paper[3] on the limits for finding a quantum theory of everything is another lens.

Yet another path is through Type 2 TMs and the Borel hierarchy, where while you can have a uncomputable number on the input tape you algorithms themselves cannot use them, while you can produce uncomputable numbers by randomly selecting and/or changing an infinite sequence.

Really it is the difference between expressability and algorithms working within what you can express.

Hopefully someone else can provide more accessible resources. I think a partial understanding of the limits of algorithms and computation will become more important in this new era.

[1] https://arxiv.org/abs/chao-dyn/9407003 [2] https://arxiv.org/abs/1804.05495 [3] https://arxiv.org/abs/2505.11773

Re: BusyBeaver(6) Is Quite Large

#63

Post by bo1024 »

ChadNauseam wrote: post #11
Scarblac wrote: post #4

It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.

The number itself is not independent of ZFC. (Every integer can be expressed in ZFC.) What's independent of ZFC is the process of computing BB(748).

I think the more correct statement is that there are different models of ZFC in which BB(748) are different numbers. People find that weird because they don't think about non-standard models, as arguably they shouldn't.

Re: BusyBeaver(6) Is Quite Large

#65

Post by MichaelDickens »

It's known that BB(14) is bigger than Graham's number, but this new finding leads me to believe that BB(7) is probably bigger than Graham's number. Intuitively, the technology required to go from pentation to Graham's number feels simpler than the technology required to go from `47,176,870` to `2 5`.

Re: BusyBeaver(6) Is Quite Large

#66

Post by LegionMammal978 »

ajkjk wrote: post #43
dtech wrote: post #24

Earlier quoted context omitted.

I am also not an expert, but this does not sound right to me. Godel's incompleteness theorem shows that there are certain things that cannot be proven. Being independent of ZFC means that something is such a case. So BB(643) being independent of ZFC means that we cannot prove or disprove that a certain number is BB(643). Aka we don't have the math to know for certain.

Yeah, but the vexing part is "how can that be true for e.g. N=643 but not N=642"? What happens at whatever number it starts true at? Incidentally, Gödel's theorem eventually comes down to a halting-like argument as well (well, a diagonal argument). There is a presentation of it that is in like less than one page in terms of the halting problem---all of the Gödel-numbering stuff is essentially an antiquated proof. I r…

> What happens at whatever number it starts true at?

Usually, "what happens" is that the machines become large enough to represent a form of induction too strong for the axioms to 'reason' about. It's a function of the axioms of your theory, and you can add more axioms to stave it off, but of course you can't prove that your new axioms are consistent without even more axioms.

> There is a presentation of it that is in like less than one page in terms of the halting problem---all of the Gödel-numbering stuff is essentially an antiquated proof.

Only insofar as you can put faith into the Church–Turing thesis to sort out all the technicalities of enumerating and verifying proofs. There still must be an encoding, just not the usual Gödel numbering.

Re: BusyBeaver(6) Is Quite Large

#68

Post by heftig »

unsnap_biceps wrote: post #48
charcircuit wrote: post #42

>imagine you had 10,000,000_10 grains of sand. Then you could … well, uh … you could fill about 10,000,000_10 copies of the observable universe with that sand. I hope that helps people visualize it! People can't visualize numbers that big. There's more ways to express numbers than just counting them. For example a single grain of sand has infinite states it can be in (there are an infinite amount of real numbers), so…

I'm confused about this example, isn't the count of grains of sand equal to the count of observable universes so it'd be a single grain of sand per universe?

The "about" does a lot of heavy lifting in this example. Dividing 10,000,000_10 by the number of grains that fit into one universe doesn't change it much. The 10,000,000 would get smaller somewhere in the deep depths of the decimal fraction.

Re: BusyBeaver(6) Is Quite Large

#69

Post by drdeca »

Scarblac wrote: post #4

It boggles my mind that a number (an uncomputable number, granted) like BB(748) can be "independent of ZFC". It feels like a category error or something.

No individual number is uncomputable. There’s no pair of a number and proof in ZFC that [that number] is the value of BB(748). And, so, there’s no program which ZFC proves to output the value of BB(748). There is a program that outputs BB(748) though, just like for any other number.

Re: BusyBeaver(6) Is Quite Large

#70

Post by Nevermark »

lupire wrote: post #30
seeknotfind wrote: post #2

> So I said, imagine you had 10,000,000sub10 grains of sand. Then you could … well, uh … you could fill about 10,000,000sub10 copies of the observable universe with that sand. I don't get this part. Is it really rounding away the volume of the observable universe divided by the average volume of a grain of sand? That is many more orders of magnitude than the amount of mass in the universe, which is a more usual compa…

Here's a more common example of this sort of comparison: In significant figures, 1.0 billion minus 1.0 million equals 1.0 billion.

True but this is a ratio.

However many universes in question, there is a qualitative difference between that many empty universes (with 1 grain), and that many completely packed with grain.

Ask anybody who lives in one!

Post reply on HN