LeanSwarm: An Agent Swarm for Long-Horizon Lean 4 Theorem Proving and Counterexample Discovery

Long-horizon theorem proving requires more than solving isolated proof states. Large developments involve evolving proof plans, auxiliary lemmas, failed decompositions, and dependencies that must persist across many proof-assistant interactions. We present **LeanSwarm**, a guide-centric multi-agent system for autonomous long-horizon theorem proving in Lean 4. Specialized agents handle proof planning, construction, repository search, research, cycle analysis, and repair, while durable proof state is maintained outside any individual agent context. When ordinary proof search stalls, the system can escalate to deeper analysis, revise the proof structure, or diagnose that a target is false or under-specified. We evaluate **LeanSwarm** on the 600-problem Lean split of NTP4VC and on long-horizon correctness proofs from Strata. On NTP4VC, **LeanSwarm** proves 563/600 (93.8%) verification conditions, which to the best of our knowledge is the highest reported end-to-end solve rate on this split. In the Strata case studies, controlled comparisons against a standalone Claude Code agent using the same primary model show faster proof development, including 25% lower wall-clock time, 12% lower cost, and 17% shorter proofs on a substantial transformation-correctness task. **LeanSwarm** also closes a previously open SMT correctness target, discovers proof architectures different from an existing human development, and identifies false or under-specified specifications that the standalone Claude Code agent continues trying to prove. These results suggest that durable state, specialization, and structured escalation substantially extend strong language models on long-horizon formal reasoning.