• Seed-Prover 是团队参与 IMO 2025 国际数学奥林匹克的官方系统，成功解决 4 道难题（P2 几何、P3 数论、P4 数论、P5 组合/代数），展示了 AI 在严谨数学证明中的实用性和高效性。
• P2 题几何证明仅用 2 秒生成并验证，P3 和 P4 题的数论证明分别用 Lean 形式化语言完成，代码行数达 2000 和 4000 行，体现深度形式化能力。
• P5 题的证明创新性强，算法生成的证明与人类传统解法存在差异，体现 AI 方法在数学创新上的潜力。
• 另有 Delta-Prover 项目，专注于测试时生成形式证明的技术研究，推动自动化数学系统的性能极限。
• 全部证明基于 Lean v4.14.0，采用 Apache-2.0 开源许可，方便社区复用与二次开发。
Seed-Prover 不仅是数学 AI 形式化证明的里程碑，也为数学研究方法论带来新的视角，推动数学与人工智能深度融合。长期来看，这类工具将成为数学家、科研人员的强力助手，实现复杂数学问题的自动验证和创新发现。
