#字节模型拿下IMO银牌##字节数学模型能复现全过程# 字节的数学推理模型Seed Prover，杀进国际数学奥林匹克（IMO 2025），拿下了银牌。 赛后它还顺手把第1题补了，等于解完了6道题中的前5题。 其中第3题和第4题，模型各花了3天，写出几千行形式化代码，真的是一行一行“死磕”的那种。 背后靠的是引理（Lemma）链（引理是比定理更次要的结果）。 通俗讲，这就是把一道大题拆成几十个小结论，每个结论都能自动验证，像搭积木一样，一层一层往上垒，直到最终通关。 而且这不是靠堆算力硬解的，Seed Prover的“重量级模式”，能自己构造新猜想、反复试错、建出一个引理池，再用里面的关键引理反向喂给自己继续推理。 相比之下，尽管DeepMind在本届IMO中解出5题拿下金牌，OpenAI实验性模型也实现类似水平，但Seed Prover的优势是“可验证”——每一行代码都能形式化复现，不存在跳步。 目前它在多个公开数学测试上都吊打SOTA（最先进模型），Putnam赛题得分翻了5倍，MiniF2F测试基本满分，就连大学组合数学题也能搞定。 Seed Prover已开源部分题目的形式化代码： 第 1 题证明： -Seed/Seed-Prover/blob/main/SeedProver/imo2025/p1.lean 第 2 题证明： -Seed/Seed-Prover/blob/main/SeedProver/imo2025/p2_proof.pdf 第 3 题证明： -Seed/Seed-Prover/blob/main/SeedProver/imo2025/p3.lean 第 4 题证明： -Seed/Seed-Prover/blob/main/SeedProver/imo2025/p4.lean 第 5 题证明： -Seed/Seed-Prover/blob/main/SeedProver/imo2025/p5.lean
