Wire the Lean 4 backend into the proof agent

[dingf3ng]

Summary

• run the proof agent end to end through ProverBackend and the Lean 4 adapter
• remove the legacy CoqInterface runtime and test path
• expose only Lean 4 in this independently testable stack tip
• add controller, CLI, rendering, cleanup, and real prover workflow coverage

Stack dependency

Draft; depends on #5. The narrow wiring-only diff is available in the fork at dingf3ng#6. Until the lower PRs merge, GitHub shows their commits here as well.

Verification

• 119 deterministic tests passed; the real Lean agent workflow and certificate replay passed in 25.32s.
• No Python reference to CoqInterface or either unrelated adapter remains.