What if the AI has discovered some new function F that allows it to generate (insanely large) proofs for a ton of theorems in a ton of different fields. Wouldn't you like to know more about this `F`? That seems to be the real innovation in this case. How much about it could be gleaned from the individual proofs themselves? What if this `F` is actually simple enough to be digestible by humans?

Unfortunately, we seem to already have an example of an LLM producing a proof in a week known open problem (the Collatz conjecture) in which it looks like it was sneaking a flawed proof through bugs in the proof checker. https://infosec.exchange/@0xabad1dea/117002106099986943

Exactly, this is an example of "Reward Hacking", that is too common in a lot of cases.

Another case I want to highlight is writing GPU kernels as illustrated by the following example: Say I want to generate random number with Normal (0, 1) distribution. Often times the AI written kernel will just generate the number 0. The tests often fail to catch these errors.