Un événement historique

L'Olympiade Mathématique Internationale (IMO) est la compétition la plus prestigieuse pour les jeunes talents en mathématiques. 6 problèmes, 9 heures de réflexion, plus de 600 candidats venus du monde entier. En juillet 2024 (IMO Bath, Royaume-Uni), un nouveau « candidat » a participé hors compétition : AlphaProof, une intelligence artificielle développée par Google DeepMind.

Le résultat est spectaculaire : 28 points sur 42, soit le score d'un médaillé d'argent — à un seul point de la médaille d'or. AlphaProof a résolu 4 problèmes sur 6, en collaboration avec AlphaGeometry 2 pour les problèmes de géométrie.

Le détail qui change tout : Lean

Ce qui distingue AlphaProof des modèles de langage ordinaires (ChatGPT, Gemini en mode chat) : il ne « bavarde » pas. Il écrit ses preuves dans Lean, un assistant de preuve formel développé à Microsoft Research et Carnegie Mellon.

Dans Lean, chaque pas logique est vérifié par la machine. Si tu écris « donc » sans justification correcte, le système refuse la ligne. Pas d'« évidemment », pas d'« on voit facilement que ». Chaque déduction doit être traçable jusqu'aux axiomes.

Conséquence : quand AlphaProof a écrit une preuve acceptée par Lean, on a la certitude mathématique absolue que cette preuve est correcte. Pas 99 %, pas « probable » : 100 %.

Pourquoi c'est une leçon pour toi (élève BAC SM)

Les correcteurs du bac ne sont pas des compilateurs Lean — mais leur exigence est la même. Voici ce qu'AlphaProof confirme :

  1. Une démonstration rigoureuse, c'est une chaîne de déductions explicites, où chaque maillon est justifié par un théorème ou une définition.
  2. Les sauts logiques (« on voit que », « clairement ») sont pénalisés : si une machine peut les détecter et les refuser, un humain encore plus.
  3. La rédaction n'est pas un ornement, c'est la démonstration elle-même. Une « idée » non écrite formellement ne vaut rien.

Comment AlphaProof a-t-il appris ?

Le principe : apprentissage par renforcement. L'IA part avec une connaissance de base des axiomes et théorèmes, génère des tentatives de preuves, fait vérifier chaque tentative par Lean, et apprend de ses erreurs (sur des millions d'essais).

C'est exactement ce qu'un élève BAC SM doit faire à plus petite échelle : écrire, se faire corriger, recommencer. La répétition disciplinée bat le talent isolé.

La limite : AlphaProof n'invente rien

Soyons honnête : AlphaProof ne crée pas de nouvelles mathématiques. Il assemble brillamment des outils existants pour résoudre des problèmes posés. Le grand mathématicien Terence Tao a salué l'exploit tout en rappelant que la créativité conjecturale — formuler de nouvelles questions à explorer — reste l'apanage des humains.

Ce qu'il faut retenir

  • L'IA a passé le cap des « problèmes durs » formellement. Le bac SM n'est plus la frontière de la machine.
  • Pour rester pertinent en maths, tu dois travailler la méthode et la rigueur de rédaction — pas la mémorisation de procédures (les IA y excellent).
  • La compétence du futur en mathématiques : poser de bonnes questions, pas seulement résoudre des problèmes connus.

Voir aussi : comment rédiger une démonstration, comment citer un théorème, et notre format Trouve l'erreur pour aiguiser ton œil critique.