Les progrès récents des modèles de langage et des outils d'assistance formelle mettent désormais l'intelligence artificielle au centre d'une discussion passionnée parmi les mathématiciens : peut‑on considérer comme satisfaisantes des « preuves » produites par des systèmes que personne ne comprend totalement ?
Des machines qui démontrent, mais qui n'expliquent pas
Des modèles d'IA ont commencé à produire des démonstrations de résultats mathématiques que des générations de chercheurs cherchaient à établir. Pour plusieurs spécialistes, dont Mickaël Randour, responsable du département de Mathématiques à l'Université de Mons et signataire de la Déclaration de Leiden, la question centrale n'est pas seulement de savoir si une preuve est correcte sur le plan formel, mais si elle rend la vérité compréhensible et réutilisable.
« L'IA, pour ces preuves très longues, utilise un langage formel très complexe, Lean. Ces preuves ne sont pas du tout faites comme le ferait un mathématicien. »
La référence au langage formel Lean illustre bien le phénomène : ces outils traduisent un raisonnement en une suite de vérifications formelles qui garantissent, techniquement, la validité. Mais, selon Randour, ils n'éclairent pas les grandes étapes intellectuelles qui permettent à l'humain de saisir, d'enseigner et de prolonger le résultat.
Comprendre vs valider : une tension épistémologique
Le débat dépasse une simple querelle de méthode. Plusieurs mathématiciens, parmi lesquels le médaillé Fields Hugo Duminil‑Copin, estiment que le cheminement intellectuel — l'effort, l'intuition, la construction progressive des idées — est aussi précieux que la conclusion. Duminil‑Copin compare l'usage exclusif de l'IA pour obtenir un résultat au fait de se faire héliporter au sommet de l'Everest plutôt que d'en gravir les pentes : l'expérience et l'apprentissage disparaissent.
Ce questionnement s'accompagne d'observations pratiques. Amaury Hayat signale déjà des dérives : des soumissions à des revues scientifiques rédigées complètement par des IA, et dont les auteurs humains, d'après lui, ne maîtrisent pas le contenu. Ces pratiques inquiètent pour l'intégrité de la recherche et la formation des jeunes scientifiques.
Conséquences pour la recherche et l'enseignement
Plusieurs enjeux se dégagent :
- Perte de compréhension : des preuves formellement correctes mais « opaques » peuvent empêcher la transmission des idées et la construction de nouveaux résultats.
- Compétences cognitives : l'apprentissage et l'entraînement du raisonnement mathématique risquent d'être négligés si l'on compte trop sur des outils automatisés.
- Intégrité scientifique : l'utilisation d'IA pour rédiger des articles ou produire des preuves sans maîtrise humaine soulève des questions éthiques et éditoriales.
| Préoccupation | Conséquence |
|---|---|
| Opaque preuve formelle | Difficulté à extraire une intuition réutilisable |
| Dépendance aux outils | Affaiblissement des compétences en raisonnement |
| Soumissions non maîtrisées | Risque pour la qualité des publications |
Vers quelles réponses ?
Les interventions récentes montrent que la communauté mathématique prend la question au sérieux. La Déclaration de Leiden incite à la vigilance et à des règles d'usage de l'IA dans la recherche. Sur le plan pédagogique, plusieurs intervenants rappellent la nécessité de continuer à « exercer son cerveau », par l'apprentissage traditionnel des méthodes et de la rigueur : avant d'utiliser une calculatrice, on apprend le calcul mental, résument-ils.
Pour l'instant, la technologie met en évidence une tension entre validation automatisée et compréhension humaine. Les acteurs universitaires et éditoriaux devront définir des cadres permettant d'exploiter les capacités de l'IA sans perdre la capacité à expliquer, critiquer et prolonger les découvertes. Sans cette clarification, les preuves produites par des systèmes complexes risquent de rester des certificats de conformité plutôt que des leviers de progrès scientifique.
La discussion est loin d'être close. Elle affectera non seulement la pratique des mathématiques pures, mais aussi la formation des futurs chercheurs et la confiance du public dans la science. Les prochains mois seront sans doute l'occasion d'élaborer des standards et des bonnes pratiques — à la fois techniques et pédagogiques — pour intégrer l'IA sans sacrifier la compréhension.
