Mathématiques : quand l’intelligence artificielle défie le génie humain

Les résultats tombent comme une équation bien résolue: en 2025, plusieurs intelligences artificielles ont décroché des médailles d’or aux Olympiades internationales de mathématiques, la compétition la plus exigeante au monde. Parmi les lauréats : Gemini de Google, Seed-Prover de ByteDance (propriétaire de TikTok) et Aristotle, développé par la start-up américaine Harmonic.

Ces systèmes ont triomphé sur presque toutes les épreuves, ne butant que sur un problème combinatoire complexe de pavage du plan — un exercice résolu par seulement quatre participants humains.

Un exploit symbolique, lorsqu’on se souvient qu’en 2024, AlphaGeometry, développé par DeepMind (filiale d’Alphabet), ne parvenait encore qu’à une médaille d’argent, limité aux problèmes de géométrie pure.

Des progrès remarquables en quelques années

Le rythme des avancées impressionne. En 2022, les IA plafonnaient à 30% de réussite sur les tests de référence en mathématiques, comme MATH ou miniF2F. Trois ans plus tard, les modèles de dernière génération – Gemini 2.5, GPT, Llama 3 ou DeepSeek – dépassent les 95 %, voire 99 % de réussite sur certaines épreuves.

Pour Amaury Hayat, professeur à l’École nationale des ponts et chaussées, citée par Le Monde, ces performances ne sont pas anodines "Les entreprises de l’IA considèrent les mathématiques comme un terrain d’évaluation idéal pour mesurer la véritable intelligence de leurs modèles. C’est aussi une vitrine technologique qui leur permet d’attirer les meilleurs talents".

Un "second cerveau" au service de la rigueur

Derrière ces prouesses se cache une nouvelle approche: le raisonnement par renforcement. Les modèles apprennent à s’auto-corriger, testent des millions de solutions et créent leurs propres jeux de données pour combler les manques d’exemples réels.

En janvier 2024, DeepMind a frappé fort avec AlphaGeometry, doté d’un “second cerveau” virtuel capable de générer et démontrer de nouveaux théorèmes géométriques. Résultat: 25 problèmes résolus sur 30, une première. Quelques mois plus tard, son successeur, AlphaProof, entraîné sur 100 millions de démonstrations formelles en langage Lean, décrochait la médaille d’argent aux vraies Olympiades.

Le secret de sa réussite ? Une architecture mêlant apprentissage automatique et langages logico-mathématiques formels, qui permettent à la machine de vérifier la validité de ses propres preuves, ligne par ligne.

La formalisation du raisonnement, un nouvel horizon

Ces langages dits "formels"Lean, Rocq (ex-Coq) ou Isabelle, ouvrent la voie à une mathématique hybride. Conçus à l’origine pour vérifier des logiciels, ils servent aujourd’hui à certifier des démonstrations complexes, garantissant une rigueur absolue.
"Ce que l’on pensait réservé à l’intuition humaine devient vérifiable par la machine", explique au journal Le Monde Patrick Massot, chercheur à l’Université Paris-Saclay.

Des start-up comme Math, Inc. automatisent déjà la traduction des preuves en code logique, jusqu’à 25 000 lignes vérifiées par IA. Et le projet européen Malinca, lancé en 2025, ambitionne de rendre le langage mathématique “naturel” compréhensible par les machines.

Quand la machine inspire les mathématiciens

Loin d’opposer hommes et machines, une coopération inédite se dessine. En 2023, une équipe franco-américaine a utilisé une IA pour redécouvrir une loi géométrique oubliée, ouvrant la voie à de nouvelles conjectures.

D’autres chercheurs se servent des IA pour vérifier automatiquement des preuves ou explorer des branches entières de l’algèbre et de la topologie.

Ces outils deviennent ainsi les laboratoires virtuels d’une science plus rapide, plus rigoureuse, mais aussi plus collective.

Les spécialistes sont catégoriques, les IA ne remplaceront pas les mathématiciens. Mais elles redessinent le paysage de la recherche, accélèrent les découvertes et posent de nouvelles questions philosophiques.