Ceci est le document IMO de ByteDance dont j'ai entendu parler récemment. Ils ont construit des systèmes hybrides qui utilisent Lean ainsi qu'un LLM. Ils ont pu résoudre 5/6 problèmes en utilisant les deux systèmes Seed-Prover et Seed-Geometry (qui améliore les capacités géométriques faibles de Lean). Si j'ai bien compris, seul Seed-Prover a participé officiellement à l'IMO et a résolu 4/6 pour une médaille d'argent.