>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