Hacker News Reader

If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.

View on HN

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.

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?

Reply on news.ycombinator.com