Dies ist das ByteDance IMO-Papier, von dem ich kürzlich Gerüchte gehört habe. Sie haben hybride Systeme entwickelt, die sowohl Lean als auch ein LLM verwenden. Sie konnten 5 von 6 Problemen mit den beiden Systemen Seed-Prover und Seed-Geometry lösen (was die schwachen Geometriefähigkeiten von Lean verbessert). Soweit ich verstehe, hat nur Seed-Prover offiziell an der IMO teilgenommen und 4 von 6 für eine Silbermedaille gelöst.