ICM 2026 Plenary Lecture - Alex Kontorovich

Dans cette conférence plénière de l’ICM 2026, Alex Kontorovich, professeur à Rutgers, expose sa vision de l’évolution des mathématiques avec l’essor de l’intelligence artificielle et des outils de formalisation. Il commence par rappeler son expérience avec les systèmes de calcul formel, puis introduit les grands modèles de langage (LLM) comme des processus stochastiques générant du texte plausible, mais non fiable pour la rigueur mathématique. Il oppose cette approche à celle des prouveurs interactifs comme Lean, qui vérifient chaque étape d’une preuve. Il démontre l’utilisation de Lean sur un exemple simple, soulignant que le prouveur ne fait pas les preuves à la place du mathématicien, mais valide son raisonnement. Il aborde ensuite les défis de la formalisation, notamment l’alignement sémantique et les risques de triche des LLM. Il présente le concept de ‘Mathlib halo’ pour désigner les ouvrages formalisables grâce aux prérequis déjà présents dans la bibliothèque Mathlib. Il conclut en évoquant les perspectives pour la recherche et l’enseignement, insistant sur la nécessité pour les mathématiciens de rester responsables de leurs affirmations, quel que soit l’outil utilisé.