« Dissoudre plutôt que résoudre » la complexité : une formule qui me semble dire quelque chose de la manière dont l'IA vient assister le travail de nos chercheurs et ingénieurs.
Merci Flavien de mettre en lumière cette incroyable percée, et plus largement la transformation silencieuse mais déterminante du rapport entre mathématiques, preuve formelle et intelligence artificielle. Il y a déjà 50 ans, la preuve du théorème des quatre couleurs avait eu recours à un ordinateur, chargé de vérifier des milliers de configurations. Ce que nous voyons aujourd'hui, c'est la même logique démultipliée par les langages formels : une capacité accrue à explorer, dissoudre, reconstruire un paysage de preuves.
Ces dernières avancées de l'IA dans le domaine des mathématiques m'inspirent trois réflexions.
D'abord les progrès époustouflants des modèles spécialisés—comme KimiK2Thinking ou DeepSeekMath-V2—qui définissent de nouveaux standards dans les benchmarks de raisonnement mathématique. Mais au-delà des performances, Math-V2 serait particulièrement fascinant par son architecture en boucle duale : un modèle dédié à la résolution, un second pour la vérification. À mesure que la démonstration progresse, la part de compute allouée au vérificateur augmente dynamiquement, le système déplaçant son attention vers ce qui peut faire échouer la preuve—plus l'argument avance, plus il est mis à l'épreuve. Une stratégie qui écho au principe de Test-Driven Development où les tests software guident la construction même de la solution. Une approche artisanale dans l'esprit, mais déployée ici à une échelle computationnelle vertigineuse.
Je suis ainsi frappé par la convergence entre software engineering et mathématiques avancées : un langage comme LEAN, utilisé à la fois pour démontrer des conjectures ouvertes ou valider formellement la robustesse de logiciels critiques, incarne cette jonction étonnante entre abstraction mathématique et ingénierie des infrastructures de notre quotidien. De même, l'avènement fulgurant des LLMs a créé un point de contact inédit entre les probabilités, la logique, l'apprentissage statistique et l'ingénierie logicielle—des disciplines longtemps séparées.
Enfin, il s'opère un tournant majeur en matière d'accessibilité du savoir mathématique : ces modèles de pointe—pour la plupart open-source—mettent en œuvre des possibilités de raisonnement autrefois réservées à quelques équipes d'élite, désormais encapsulées, partagées en une forme d'intelligence mathématique « distribuée » au service de la recherche.
Nous assistons sans doute à une transformation profonde : les mathématiques ne deviennent certainement pas plus « faciles »—c'est peut-être même l'inverse, tant le niveau mathématique s'effondre dans beaucoup de pays autrefois renommés pour leur école mathématique—mais elles apparaissent beaucoup plus explorables. Et l'espace des conjectures devient un terrain où humains et machines peuvent collaborer autrement.
