Le 21 octobre, Microsoft Research a indiqué que Xinzhi Zhang et Zhao Song avaient démontré la conjecture de Kannan–Lovász–Simonovits, un problème mathématique posé en 1995. Dans l’annonce de Microsoft Research, l’entreprise affirme que le résultat provient d’un workflow d’agents piloté par des humains, plutôt que de l’exécution d’un modèle entièrement autonome.
Microsoft indique que des systèmes d’IA ont exploré plus de 100 approches candidates, tandis que les chercheurs sélectionnaient les pistes à poursuivre, écartant les voies faibles et vérifiant les résultats mathématiques restants. L’entreprise ajoute que des tentatives non guidées avec plusieurs modèles de premier plan et un budget total de tokens comparable n’ont pas résolu le problème.
Selon le billet, les outils ont été utilisés au-delà de la génération d’idées, notamment pour les dérivations, la rédaction de l’article et des vérifications internes de la preuve. Microsoft précise qu’une formalisation Lean 4 a déjà été publiée, et qu’une version plus courte, vérifiée par machine, est prévue après l’examen final.
Il reste préférable de considérer ce résultat comme un préprint important, et non comme une avancée déjà établie dans les manuels. Des sources indépendantes ont indiqué que d’autres groupes avaient publié des preuves parallèles quelques jours plus tard, ce qui renforce la confiance, mais le travail n’a pas encore fait l’objet d’une évaluation par une revue scientifique.