這是我最近聽到的有關字節跳動 IMO 論文的傳聞。他們建立了混合系統，使用 Lean 和 LLM。他們能夠使用兩個系統 Seed-Prover 和 Seed-Geometry 解決 5/6 的問題（後者改善了 Lean 幾何的弱能力）。 根據我的理解，只有 Seed-Prover 正式參加了 IMO，並解決了 4/6 的問題，獲得了銀牌。