Este é o artigo da ByteDance IMO sobre o qual ouvi rumores recentemente. Eles construíram sistemas híbridos que usam Lean e LLM. Eles foram capazes de resolver problemas 5/6 usando os dois sistemas Seed-Prover e Seed-Geometry (que melhora as capacidades fracas da geometria Lean). O único Seed-Prover do IIUC participou oficialmente da IMO e resolveu 4/6 para uma medalha de prata.