这是我最近听说的字节跳动IMO论文。他们构建了混合系统，使用了Lean和一个大型语言模型（LLM）。他们能够利用这两个系统Seed-Prover和Seed-Geometry（后者改善了Lean的几何能力）解决5/6个问题。 如果我理解正确，只有Seed-Prover在IMO上正式参与，并解决了4/6个问题，获得了银牌。