Scaling Lean Theorem Proving for Real-World Code Verification.

arXiv:2610.38174v1 Announce Type: cross Abstract: We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier