It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable.

For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.

Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.

Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.

▲

Timpanzee 23 minutes ago | parent | next [-]

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.

	▲	srcreigh 10 minutes ago \| parent \| 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". There are more interesting theorems, I want to know whether we can prove or disprove other more interesting theorems. The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". 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. 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.
	▲	moomin 18 minutes ago \| parent \| prev [-]
		Pretty sure Gödel’s theorems imply the halting problem if you squint hard enough.

▲

ogogmad 3 minutes ago | parent | prev [-]

The problem with what you're saying is that a random true proposition about the integers is not necessarily interesting enough to be called a theorem. GIT does not provide limitations on proving theorems - but about limitations on determining whether a proposition is true or not. Most propositions are ugly and boring. GIT is irrelevant.