Comment by charcircuit
17 hours ago
>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".
I feel like knowing something is true is useful, but if you don’t understand how and why, you won’t understand the implications