OpenAI démontre la conjecture de Cannon : l'IA vient à bout d'un problème de théorie géométrique des groupes vieux de près de 40 ans, avec vérification machine en Lean
Parmi les manuscrits de mathématiques publiés par OpenAI le 6 octobre, un article de 31 pages affirme démontrer entièrement la conjecture de Cannon, accompagné d'une vérification formelle en Lean.