Even if the busy beaver sequence were computable and the halting problem were decidable, Gödel's incompleteness theorems would still prevent all theorems from being solved, regardless of if one used LLMs or not.

▲

IsTom 11 minutes ago | parent | next [-]

Even more concretely, the halting problem for turing machines with halting problem oracle would be undecidable for them. And if you could solve that you won't believe what problem would be undecidable. It's turtles all the way up.

▲

srcreigh an hour ago | parent | prev | next [-]

I think there's a really important sense in which Godel's argument is not the full story.

IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific.

Another way to view it is, who cares if we can't prove or disprove "This statement is false". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about.

The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And we know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of.

So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference!

The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.

	▲	gf000 an hour ago \| parent [-]
		But a 432-state TM is a problem that we would like to "prove" is it not? It's not even a particularly complex one to begin with, my smartwatch has orders of magnitude more state then that and yet here we see that all of our math "fails" at it. I'm no mathematician, but this is also the crux of Gödel's theorem, he just showed it in a more "hacky" and clever way - but BB(432)'s relation to ZF is also a consequence of Gödel's more general idea, is it not?

▲

moomin an hour ago | parent | prev [-]

Pretty sure Gödel’s theorems imply the halting problem if you squint hard enough.