Comment by pron

> eventually finding a proof using guided search (machines searching for proofs, multiple inference attempts) takes more effort than verifying a proof. Formal verification does not disappear, because communicating a valuable succinct proof is much cheaper than having to search for the proof anew. The proofs will become inevitable lingua franca (like it is among capable humans) for computers as well. Basic economics will result in adoption of formal verification.

But AI isn't used to verify the proof. It's used to find it. And if it can find it - one of the hardest things in software development - there's no reason to believe it can't do anything else associated with software development. If AI agents find formal verification helpful, they would probably opt to use it, but there would also be no need for a human in the loop at all.

> It is currently already much better than the average human at finding proofs.

The average human also can't write hello world. LLMs are currently significantly worse at finding proofs than the average formal-verification person (I say this as someone who's done formal verification for many years), though, just as they're significantly worse at writing code than the average programmer. I'm not saying they won't become better, it's just strange to expect that they'll become better than the average formal-verification person and at the same time they won't be better than the average product manager.

> there will always be problems it can not instantly generate provably correct software

Nobody said anything about "instantly". If the AI finds formal verification helpful, it will choose to use it, but if it can find proofs better than humans, why expect that it won't be able to do easier tasks better than humans?