you've just written down 'Busy Beaver' without breaking the universe. the concept is there and it's separate from its computed value. the LLM doesn't have to compute anything to be able to work with the concept of it just as you or me. symbolic computation is nothing new even in pre-LLM AI and indeed LLMs aren't bad at working with it (MLOC lean proofs should be proof enough!)

▲

srcreigh a day ago | parent [-]

At high enough N, ZFC is independent of BB(N), and in fact any math axiom system has such an N.

The LLM itself is finite, the axioms it knows are fixed, there is an N where BB(N) is independent of those axioms, so the LLM cannot solve it.

▲

baq a day ago | parent [-]

it might know all this is my point and it can reason about it regardless.

	▲	srcreigh a day ago \| parent [-]
		The point is that it has limits in what tools it can use by virtue of being a finite program. Those limits imply that there are some math problems that it cannot solve. The LLM can know about this (and frontier LLMs likely do), but that doesn't mean it will be able to solve the math problems. To put another way, if it were true that some fixed LLM could solve every math problem, it would implement Halt, which is impossible.