Ce que signifie être mathématicien quand l'IA fait les calculs

Alors que l'intelligence artificielle s'impose progressivement dans presque tous les domaines scientifiques, la question de la place du mathématicien humain devient de plus en plus pressante. Des systèmes comme AlphaProof de DeepMind ou les grands modèles de langage actuels sont désormais capables de résoudre des problèmes de niveau olympiade, de vérifier des preuves formelles et d'assister des chercheurs sur des démonstrations qui auraient autrefois requis des années de travail. Là où un doctorant en mathématiques appliquées pouvait passer des mois à simuler des interactions optiques dans des cristaux liquides, un outil d'IA accomplit aujourd'hui un travail comparable en quelques heures. Ce changement de rythme, autrefois impensable, redéfinit concrètement ce que signifie "faire des mathématiques".

Ce qui est en jeu dépasse la simple question de productivité. Pour des générations de mathématiciens, la valeur de leur discipline ne résidait pas dans le résultat, mais dans le chemin parcouru pour y parvenir. Jeremy Avigad, chercheur à l'université Carnegie Mellon, décrit ce moment où une démonstration "se met soudainement en place" après des semaines de réflexion intensive comme une expérience à la fois esthétique et presque physique, comparable à l'achèvement d'un marathon. Si l'IA automatise ce processus, c'est cette expérience centrale qui disparaît, et avec elle une partie de ce qui donne sens à la pratique mathématique pour ceux qui l'exercent. Pour la communauté scientifique, cela soulève une question plus fondamentale encore : une preuve générée par une machine, que personne ne peut véritablement suivre pas à pas, est-elle vraiment une preuve au sens épistémologique du terme ?

La relation entre mathématiques et machine ne date pas d'hier. Dès 1976, la démonstration du théorème des quatre couleurs, toute carte peut être coloriée avec au plus quatre couleurs sans que deux régions adjacentes partagent la même, fut accomplie par un ordinateur vérifiant 1 936 cas distincts, provoquant une vive controverse dans la communauté mathématique sur la légitimité d'une telle preuve. Cinquante ans plus tard, les IA ne se contentent plus de vérifier : elles proposent des stratégies, formulent des conjectures et comblent des lacunes dans des raisonnements humains. Des chercheurs comme Krystal Maughan, doctorante en mathématiques et informatique à l'université du Vermont, soulignent que la dimension collective et lente de la discipline, ces longues heures de silence partagé avant qu'une idée émerge, reste irremplaçable. Mais la pression s'intensifie : si l'IA finit par rendre le labeur du mathématicien superflu, c'est toute une culture du raisonnement rigoureux et créatif qui devra se réinventer.