logoalt Hacker News

charcircuit • today at 6:02 AM • 1 reply • view on HN

>the economically dominant strategy to not verify them and not double check them

In the big scheme of things is it really that expensive to verify it if a lean proof is generated? The agent itself will likely have already verified such Lean code before calling it "done".


Replies

maxldn • today at 8:49 AM

I feel like knowing something is true is useful, but if you don’t understand how and why, you won’t understand the implications