Hacker News Reader

Comment by dpark | Hacker News Reader

> something that probably won’t be solved in our lifetime

If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.

I don’t know what it looks like to get to fully provable code, but I don’t see that it’s fundamentally impossible in my lifetime. Especially depending on scope. Will an entire operating system and everything on it be fully proven correct in my lifetime? Maybe not. Could the authentication stack for a product be entirely proven correct? Sure. I can’t believe that.

View on HN

> If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.

A single PC can solve a very complex simulation model in seconds, something that would require years using humans to do. Same as solving a very complicated maze. So if coupling a text generator with a proof verifier is now capable of coming up with a proof, I’m not particularly surprised. But given the cost, and the actual usefulness of the proof, I’m not particularly excited either.

But code is not a closed system, even if we do prove a lot of the internal mechanism, we still can’t know the input (noise), and whether the axiomatic foundation will hold. That’s the reason people don’t bother. The theory of computation is just too loose in its constraints. You just write enough tests to catch egregious errors.

> we still can’t know the input (noise)

Doesn't matter. Just like you can prove something is true for all numbers, you can prove something is true for all possible inputs.

> But code is not a closed system

Code is absolutely a closed system.

"Software" might not be, and definitely not software systems -- but code can have each part of it atomically proven to be correct, assuming you test it with a sufficiently complex simulation model (which you've already granted is within the possibilities for LLMs).

Prove all the code in the software system correct, then prove their interactions are correct, and you've achieved your goal.

(I won't claim this is inevitable with the current tools, but it's at least within the realm of possibility)

Reply on news.ycombinator.com