Seed-Prover

Tech stack & purpose

Seed-Prover is a collection of formal theorem-proving systems developed by ByteDance's Seed team for solving mathematical problems in Lean 4. The repository contains three related projects: Seed-Prover 1.5, Seed-Prover 1.0, and Delta-Prover. Seed-Prover 1.5 uses large-scale agentic reinforcement learning to train a formal theorem-proving model and achieves 88% success on PutnamBench (undergraduate-level problems) and solved 11 of 12 Putnam 2025 competition problems. Seed-Prover 1.0, the system used in IMO 2025, employs multi-agent inference with long chain-of-thought reasoning on the Lean verifier and solved 4 out of 6 IMO problems. Delta-Prover, a separate research project, focuses on test-time techniques for generating formal proofs and achieves 95.9% on the miniF2F-test benchmark using a custom domain-specific language layered on Lean 4 to enable reflective decomposition and iterative repair.

Community & reference links

• Arxiv
• arxiv.org/abs/2507.23726
• arxiv.org/abs/2512.17260
• huggingface.co/datasets/l3lab/miniCTX-v2

Languages

Contributors

• 
  xiaoranjin-bd14 commits · 3 followers
• 
  YichiZhou-bytedance11 commits · 13 followers
• Zheng Yuan3 commits