Chaque été, les meilleurs lycéens du monde se retrouvent pour l'Olympiade internationale de mathématiques (IMO en anglais). Six problèmes, deux jours, une difficulté redoutable : seuls des élèves d'exception parviennent à décrocher une médaille. Mais en 2024, un concurrent inattendu s'est invité dans la compétition : une intelligence artificielle. Et le résultat a surpris le monde entier.

Que s'est-il passé exactement ?

En juillet 2024, les chercheurs de Google DeepMind ont fait plancher deux systèmes d'IA, baptisés AlphaProof et AlphaGeometry 2, sur les six problèmes de l'IMO de cette année-là. Le bilan est impressionnant : l'IA a résolu quatre des six problèmes, avec des démonstrations complètes et vérifiées. Son score correspondait au niveau d'une médaille d'argent, à seulement un point du seuil de la médaille d'or.

Pour mesurer l'exploit : ces problèmes ne consistent pas à appliquer une formule. Ils demandent de l'imagination, des idées astucieuses, parfois plusieurs heures de réflexion à des humains très entraînés. Voir une machine y arriver était impensable il y a seulement quelques années.

Comment une IA peut-elle « faire des maths » ?

On pourrait croire que l'IA a simplement « deviné » les réponses. En réalité, le fonctionnement est bien plus rigoureux, et c'est ce qui rend le résultat solide.

Des preuves formelles, pas des intuitions floues

Le cœur d'AlphaProof repose sur un langage informatique appelé Lean. Lean est ce qu'on appelle un assistant de preuve : c'est un logiciel dans lequel chaque étape d'un raisonnement mathématique doit être écrite de façon tellement précise que l'ordinateur peut vérifier qu'elle est parfaitement correcte, sans la moindre ambiguïté.

Autrement dit, l'IA ne se contente pas d'annoncer un résultat : elle construit une démonstration que la machine peut contrôler ligne par ligne. Impossible de tricher ou de "sauter une étape", comme on est parfois tenté de le faire dans un devoir.

Une recherche guidée, façon jeu de stratégie

Pour trouver ces preuves, AlphaProof explore un nombre gigantesque de chemins de raisonnement possibles. À chaque étape, il se demande : quelle affirmation puis-je démontrer maintenant pour me rapprocher du but ? Cette stratégie ressemble à celle utilisée par les IA championnes du jeu de go ou des échecs : essayer, évaluer, ajuster, recommencer.

De son côté, AlphaGeometry 2 est spécialisé dans les problèmes de géométrie. Il combine deux talents : un moteur logique capable de manipuler des points, des droites et des angles, et un module qui suggère des constructions astucieuses (comme tracer une parallèle ou un cercle bien choisi) — exactement le genre d'éclair de génie qui débloque un exercice difficile.

  • AlphaProof : algèbre, théorie des nombres, problèmes généraux, via le langage Lean.
  • AlphaGeometry 2 : géométrie, en combinant logique et suggestions de constructions.
  • Point commun : chaque preuve produite est vérifiable par la machine, donc certaine.

Faut-il s'inquiéter ? L'IA va-t-elle remplacer les mathématiciens ?

C'est la question naturelle. La réponse est nuancée, mais plutôt rassurante.

D'abord, l'IA a été nettement plus lente qu'un humain : là où les élèves disposent de quelques heures, certains problèmes ont demandé à la machine plusieurs jours de calcul. Ensuite, elle a échoué sur deux problèmes — souvent ceux qui exigeaient l'idée la plus surprenante. Enfin, et c'est essentiel : l'IA ne comprend pas les maths comme nous. Elle ne ressent pas la beauté d'une démonstration, ne devine pas pourquoi un résultat est important, et ne sait pas inventer de nouvelles questions intéressantes.

Les mathématiciens voient surtout dans ces outils un assistant puissant : un partenaire capable de vérifier des calculs fastidieux, de tester des pistes, ou de débusquer une erreur dans un raisonnement. Un peu comme la calculatrice n'a pas tué le calcul, mais a libéré du temps pour réfléchir aux idées.

Et toi, élève, qu'est-ce que ça change ?

Si une machine atteint le niveau d'une médaille d'argent, à quoi bon apprendre les maths ? La réponse tient en un mot : la compréhension.

L'IA est forte parce que des humains lui ont appris à raisonner de façon rigoureuse. Ce que la compétition de 2024 montre, ce n'est pas que les maths deviennent inutiles, mais au contraire que la logique et la démonstration sont au cœur de tout. Savoir pourquoi une propriété est vraie, construire un raisonnement sans trou, justifier chaque étape : ce sont précisément les compétences que l'IA exécute... et celles qu'on te demande de développer.

Quelques pistes pour en tirer parti dans ta scolarité :

  • Soigne tes démonstrations. Comme Lean, exige de toi-même que chaque étape soit justifiée. C'est le meilleur entraînement.
  • Utilise l'IA comme un tuteur, pas comme une réponse toute faite. Demande-lui d'expliquer une notion, puis refais le raisonnement seul.
  • Cultive ta curiosité. Inventer de bonnes questions, c'est exactement ce que la machine ne sait pas faire.

Prends par exemple une identité aussi simple que : une IA la manipule en un instant, mais c'est toi qui dois comprendre pourquoi elle fonctionne et quand l'utiliser. C'est là que se joue la vraie maîtrise.

En résumé

L'exploit d'AlphaProof et d'AlphaGeometry à l'IMO 2024 est une étape marquante : pour la première fois, une IA a atteint le niveau d'une médaille d'argent sur des problèmes pensés pour les meilleurs lycéens du monde. Mais derrière la prouesse technique se cache une bonne nouvelle pour toi : les maths restent une aventure profondément humaine, faite de compréhension, de créativité et de plaisir à comprendre. L'IA est un outil formidable ; à toi de rester celui qui dirige la réflexion.