Fin 2024, AlphaProof décroche l’argent aux Olympiades Internationales de Mathématiques. Début 2025, Gemini Deep Think remporte l’or. Mais au-delà du symbole, c’est tout le rapport de l’IA à la démonstration et à la recherche mathématique qui vient de basculer.

AlphaProof : la révolution de la preuve formelle

AlphaProof repose sur une idée radicale : au lieu de produire du texte mathématique en langage naturel (comme le font les mathématiciens depuis des siècles), il formalise intégralement le problème dans Lean 4, un langage assistant de preuve.

Concrètement, voici ce qui se passe. Chaque étape de raisonnement est traduite en code formel. La machine vérifie chaque ligne, éliminant toute ambiguïté ou erreur logique. Le système combine apprentissage par renforcement et exploration heuristique des chemins de preuve — comme s’il écartait les impasses et se concentrait sur les voies prometteuses.

Résultat : des démonstrations certifiées, reproductibles, et surtout, incontestables. Aucun doute possible. Aucune relecture humaine requise.

Gemini Deep Think : quand l'IA emprunte le chemin de la pensée

À peine quelques mois plus tard, Gemini Deep Think adopte une approche radicalement différente. Plutôt que de formaliser d’emblée, le système utilise une méthode de raisonnement en chaîne approfondi (« Chain-of-Thought » étendu) qui ressemble davantage à celle d’un mathématicien griffonnant sur un tableau.

Il génère plusieurs lignes de raisonnement et les évalue en interne. Il fonctionne en langage naturel, sans recours systématique à un formalisme rigide. Et pourtant, le résultat parle : 35/42 à l’IMO 2025, soit une médaille d’or.

Deux philosophies qui semblaient incompatibles — la formalisation stricte et la flexibilité du langage naturel — deviennent soudain complémentaires.

Lean 4 : l'infrastructure qui refonde les mathématiques

Lean 4 n’est pas qu’un langage de programmation. C’est un assistant de preuve qui certifie mathématiquement chaque théorème, une révolution dans un domaine où la confiance reposait jusqu’ici sur la réputation et la relecture par les pairs.

Pourquoi cela change tout : Lean 4 garantit l’exactitude logique. Des mathématiciens de renommée mondiale comme Terence Tao l’utilisent désormais pour valider des preuves complexes. Et surtout, avant AlphaProof, formaliser manuellement une preuve prenait un temps considérable, parfois des mois. Désormais, l’IA automatise cette étape, transformant une corvée en routines.

C’est la naissance d’une mathématique machine-checkable — transparente, cumulative, et open source. Chaque résultat s’ajoute à une base de connaissance vérifiée, accessible à tous.

Au-delà des compétitions : l'IA attaque les vraies conjectures

Si les Olympiades font sensation sur les réseaux, l’impact le plus profond se situe ailleurs. Il se cache dans les conjectures non résolues depuis des décennies.

Prenez la conjecture d’Andrews-Curtis, ouverte depuis 60 ans. Une équipe de Caltech dirigée par Sergei Gukov utilise l’apprentissage par renforcement pour explorer cet espace de problèmes que les méthodes classiques ne pouvaient que contourner. L’IA n’a pas encore fourni une preuve complète, mais elle a généré de nouvelles pistes et intuitions, des chemins que personne n’avait imaginés.

De même, DeepSeek-Prover-V2 construit pas à pas une base de connaissances mathématiques vérifiées et accessibles en formalisant automatiquement des théorèmes en Lean 4. C’est un travail qui rappelle la construction lente et méthodique d’une cathédrale, pierre certifiée par pierre certifiée.

L'IA devient le copilote du mathématicien

La vraie question n’est plus de savoir si l’IA va « remplacer » les mathématiciens. C’est de comprendre comment elle va les augmenter.

Terence Tao l’explicite clairement : l’IA devient un outil de vérification ultra-rapide, de génération de cas tests et contre-exemples, de formalisation automatique de preuves complexes. Le métier de mathématicien n’est pas menacé ; il évolue. Vers plus de collaboration. Vers plus de confiance computationnelle.

Les limites à ne pas oublier

Gardons un regard critique. Ce qui fonctionne brillamment, c’est la résolution de problèmes très structurés (type Olympiades) et la vérification formelle de preuves existantes. L’IA explore des vastes espaces de preuves avec une efficacité inédite.

Mais ce qui reste limité demeure réel. La consommation énergétique est importante. La généralisation sur des problèmes faiblement formalisés reste difficile. Et l’interprétabilité des raisonnements produits, surtout avec Gemini, pose encore question. Ces systèmes ne vous expliquent pas toujours pourquoi ils ont choisi une direction plutôt qu’une autre.

L’IA mathématique est un outil prodigieux. Mais encore coûteux et spécialisé.

2025 : l'année où les mathématiques sont devenues collectives

2025 ne restera pas dans l’histoire comme l’année où « l’IA a battu les humains en maths ». Ce sera celle où l’IA a apporté la certification automatique, la formalisation à grande échelle, et de nouvelles intuitions sur des problèmes ouverts.

Les mathématiciens gardent toute leur place. Leur discipline devient plus exigeante, plus fiable, et peut-être plus collective. La preuve n’est plus une affaire de génie solitaire. C’est un travail d’équipe, où les intuitions humaines dialoguent avec la rigueur machine.

FAQ

AlphaProof et Gemini Deep Think ont-ils vraiment gagné une médaille aux Olympiades ?

Oui. AlphaProof a décroché l’argent fin 2024, Gemini Deep Think l’or en 2025 avec 35/42.

Lean 4, c'est quoi ?

Un langage formel qui permet de certifier des preuves mathématiques via vérification automatique.

L'IA peut-elle déjà résoudre des conjectures non démontrées ?

Pas encore de preuve complète, mais elle génère des intuitions nouvelles sur des problèmes ouverts.