Hacker News Reader

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!)

View on HN

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.

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

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.

Reply on news.ycombinator.com