> I think it’s broadly unclear whether (3) is true: i.e. whether frontier AI models aren’t generating or can’t generate new mathematical ideas. ... I give basically zero credence to the idea that AIs are incapable of this because of some intrinsic feature of how LLMs work.

LLMs are computer programs, so there are math problems which they cannot solve. AKA, ideas which are not possible for them to generate.

The argument for this is that Busy Beaver function is uncomputable. More specifically, some N-state Turing machine requires a proof that it doesn't halt. At some point N is too large and LLM being a computer program, it cannot generate the required proof.

See the Busy Beaver Frontier [1]

This is VERY DIFFERENT from the Halting Problem. In the Halting Problem, we see that no computer can decide whether an arbitrary given input program halts. With the argument above, for a fixed LLM, there is specific math problem which is beyond the capability of proof by the LLM (though other LLMs or humans could perhaps prove it).

Humans are not bound by the argument since we aren't finite computer programs (no proof for this anyways). LLMs which "evolve" over time with input from the natural world also aren't bound by this, since their code is effectively infinite. The argument only applies to a static program with fixed input, no dynamic information sources.

Some people believe in divine inspiration. Maybe you could believe that humans incorporate information from the natural world which LLMs don't have access to. Either of these beliefs would imply that humans have an edge.

[1]: https://www.scottaaronson.com/papers/bb.pdf

▲

baq a day ago | parent | next [-]

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.

▲

im3w1l a day ago | parent | prev [-]

A very simple program that loops over all strings and feeds them into a proof verifier should eventually prove every statement that can be proven, as far as I can tell?

▲

QuadmasterXLII a day ago | parent | next [-]

No proof verifier verifies all valid proofs and terminates on all invalid proofs.

(actually I am wrong. You would introduce a new proof, and then step the verifier on all ongoing proofs, so non-termination isn't a driving concern)

▲

ifdefdebug a day ago | parent | prev | next [-]

No. Whenever you are done with all strings of length n, you still have to check all strings of length n+1. So that moment you identify by "eventually" can never be reached.

	▲	im3w1l a day ago \| parent [-]
		If something can be proven there is a finite length proof, and if you check lengths one by one eventually you will reach a high enough length for a valid proof.

▲

srcreigh a day ago | parent | prev [-]

No, but you hit the nail on the head, that’s the most interesting part.

The proof verifier uses fixed math axioms. The busy beaver function at high enough N cannot be proven with those axioms.

▲

im3w1l a day ago | parent [-]

I specifically said that it will prove everything that can be proven, conceding that some statements cannot be proven no matter what you do.

▲

srcreigh a day ago | parent [-]

The point is that some statements could be provable, but not with today's proof verifier.

"Everything that can be proven" is relative. PA can prove some things, ZF more things. In 200 years we could develop more powerful math foundations which can prove more things. Today's proof verifiers could never prove them, but tomorrow's proof verifiers could. And the cycle repeats.

▲

im3w1l a day ago | parent [-]

Just like turing machines are universal in the sense that they can all emulate each other, I feel like there should be some universal logic that can emulate any other logical theory. Something like the gödel numbering construction maybe? This is where my knowledge ends, I'm afraid.

▲

srcreigh a day ago | parent [-]

Nope, there is no such universal logic. Godel helped show the opposite actually (incompleteness). I think Scott Aaronson's post is very fascinating explanation of this stuff. https://www.scottaaronson.com/papers/bb.pdf

	▲	im3w1l a day ago \| parent [-]
		I don't think incompleteness disproves my idea, at least not trivially. Let's take the case of ZF vs ZFC. I would say that ZF can simulate ZFC. To create a simulation we want a function f from statements in ZFC to statements in some subset of ZF so that valid inferences in one correspond to valid inferences in the other. This is quite simple. f(p) = C implies p does the job quite elegantly. Interestingly it's harder to do the opposite, to simulate ZF in ZFC, because there is no way to express "forget that you know about C". Such a construction cannot be possible in general because if a contradictory axiom is added, then everything is true, and a theory where everything is true is useless and can't simulate anything. However for C in particular I believe it should be possible to make such a construction but I can't immediately think of how I would do it.