Это документ IMO от ByteDance, о котором я слышал слухи недавно. Они создали гибридные системы, которые используют Lean, а также LLM. Им удалось решить 5 из 6 задач с помощью двух систем Seed-Prover и Seed-Geometry (которая улучшает слабые геометрические возможности Lean). Если я правильно понимаю, только Seed-Prover официально участвовал в IMO и решил 4 из 6 задач для получения серебряной медали.