> 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

LLMs use RNG for sampling, so they are not pure computers.

Computable includes BPP

Not sure if GPT based LLMs are polynomial time.