Seed-Prover: Advancing Automated Mathematical Reasoning with Formal Verification

The document introduces Seed-Prover and Seed-Geometry, two advanced AI frameworks developed by ByteDance for automated mathematical reasoning and theorem proving, particularly for challenging competition-level problems like the International Mathematical Olympiad (IMO). Seed-Prover specializes in formal theorem proving in Lean 4, employing a novel lemma-style approach with iterative refinement and multi-tiered inference strategies (light, medium, and heavy) to achieve state-of-the-art results on various mathematical benchmarks, including proving 5 out of 6 problems in IMO 2025. Complementing this, Seed-Geometry is a dedicated geometry reasoning engine that outperforms previous systems by utilizing an extended domain-specific language, an exceptionally fast C++ backend, and an advanced large language model, significantly improving its ability to solve complex geometry problems. The text highlights how formal verification languages like Lean provide clear supervision signals for training these powerful AI models, enabling breakthroughs in automated mathematical reasoning.