Detta är ByteDance IMO-tidningen som jag hört rykten om nyligen. De byggde hybridsystem som använder Lean samt en LLM. De kunde lösa 5/6 problem med hjälp av de två systemen Seed-Prover och Seed-Geometry (vilket förbättrar svaga Lean-geometriska egenskaper). IIUC endast Seed-Prover deltog officiellt på IMO och löste 4/6 för en silvermedalj.