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

Seed-Prover 1.5

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

• Seed Prover 1.5 Seed-Prover 1.5 is our latest formal proving system. It can solve 88% of the problems in PutnamBench and 11 out of the 12 competition problems from Putnam 2025. Arxiv
• Seed Prover Seed‑Prover 1.0 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 IMO 2025

Seed Prover 1.0 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)

Details

• 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.

Citation

@misc{chen2025seedprover15masteringundergraduatelevel,
      title={Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience}, 
      author={Jiangjie Chen and Wenxiang Chen and Jiacheng Du and Jinyi Hu and Zhicheng Jiang and Allan Jie and Xiaoran Jin and Xing Jin and Chenggang Li and Wenlei Shi and Zhihong Wang and Mingxuan Wang and Chenrui Wei and Shufa Wei and Huajian Xin and Fan Yang and Weihao Gao and Zheng Yuan and Tianyang Zhan and Zeyu Zheng and Tianxi Zhou and Thomas Hanwen Zhu},
      year={2025},
      eprint={2512.17260},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2512.17260}, 
}

@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}, 
}