>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".
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".