[rowanG077]

Once you now something is correct, with a proof. It is MUCH easier to understand why it is correct. Than to start from a slate that you don't even know whether something is correct or not. In that sense AI that can just solve high level math problems is immensely useful. It allows a mathematician to explore ideas at a much more rapid pace.

[terminalbraid]

Consider that since an LLM is really just an large encoding of data, the "proof" is in there already. All further work on it is effectively only rearranging words. Then all math an LLM is capable of is "done" and we have the "proof" in the LLM which by your definition is now "MUCH easier to understand" and this work is somehow sufficient.

Do you see the problem with your reasoning?

[rowanG077]

You're confusing "contains information" with "has produced a result."

A proof being latent in an LLM is no more significant than a proof being latent in a book, a theorem prover, or the axioms themselves. Einstein's papers were latent in the genetic code of his parents and the environment of his time. That doesn't mean general relativity was "already done" before Einstein was born.

By your logic, no computation has ever accomplished anything because the output was always implicit in the inputs.

The entire purpose of computation is extracting information from representations where it's difficult to see into representations where it's easy to see.

So no, this isn't a problem with the original reasoning. It's a problem with yours.