You can get to know us better through the following channels👇

This page is used to store the Seed AI4Math group’s research projects, including Seed‑Prover and Delta‑Prover.

• Seed Prover Seed‑Prover is the system we officially participated with in the IMO 2025. Arxiv
• Delta prover Delta‑Prover is a separate project focused on researching test time techniques for generating formal proofs. Arxiv

Seed Prover solved 4 out of 6 problems in IMO 2025 durint the context, with the following breakdown:

• Day 1: Fully solved P2 (geometry) and P3 (number theory), fully solved P1 (combinatorics) after the competition.
• Day 2: Fully solved P4 (number theory) and P5 (combinatorics / algebra)

• P1 (combinatorics) Lean : Fully proved after the competition, this is not scored by the IMO.
• P2 (geometry) NL : Generated and verified in 2 seconds using Seed-Geometry system
• P3 (number theory) NL Lean: Solved in 3 days, with a 2000-line formal proof
• P4 (number theory) NL Lean: Solved in 3 days, with a 4000-line formal proof
• P5 (combinatorics / algebra) NL Lean: Solved in 1 day, with a proof slightly different from known human solutions

P1,3,4,5 are compiled under Lean v4.14.0.

@misc{chen2025seedproverdeepbroadreasoning,
      title={Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving}, 
      author={Luoxin Chen and Jinming Gu and Liankai Huang and Wenhao Huang and Zhicheng Jiang and Allan Jie and Xiaoran Jin and Xing Jin and Chenggang Li and Kaijing Ma and Cheng Ren and Jiawei Shen and Wenlei Shi and Tong Sun and He Sun and Jiahui Wang and Siran Wang and Zhihong Wang and Chenrui Wei and Shufa Wei and Yonghui Wu and Yuchen Wu and Yihang Xia and Huajian Xin and Fan Yang and Huaiyuan Ying and Hongyi Yuan and Zheng Yuan and Tianyang Zhan and Chi Zhang and Yue Zhang and Ge Zhang and Tianyun Zhao and Jianqiu Zhao and Yichi Zhou and Thomas Hanwen Zhu},
      year={2025},
      eprint={2507.23726},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2507.23726}, 
}