Sans fine-tuning, une IA prouve les 6 problèmes de l'IMO 2026 en Lean

Des chercheurs de la Case Western Reserve University (travail réalisé pendant un stage chez Amazon Web Services) montrent qu'un grand modèle de langage prêt à l'emploi, sans aucun fine-tuning, peut prouver des théorèmes complexes et la correction de programmes, à condition d'organiser correctement le travail autour de lui. Ils ont choisi Anthropic Fable-5 comme modèle. Les preuves sont écrites dans Lean : dans ce langage, un petit « noyau » vérifie chaque étape du raisonnement, et il est impossible de le tromper.

Le système a résolu les six problèmes formalisés de l'Olympiade internationale de mathématiques 2026. Il est aussi venu à bout de toutes les tâches de VERINA (un jeu de programmation vérifiée) et a traité les conditions de vérification de NTP4VC, un jeu industriel de vérification formelle de code. Il résout en outre des problèmes de PutnamBench, un jeu de problèmes formalisés issus du concours universitaire Putnam.

Chaque résultat comptabilisé est soit une preuve, soit une réfutation de l'énoncé, et les deux sont vérifiées par le noyau de Lean.

Un arbre d'agents plutôt qu'une série de relances

La difficulté tient à ce que Lean ne répond qu'à une question locale : une étape donnée passe-t-elle ou non ? Un mauvais découpage du problème ou un lemme manquant (énoncé auxiliaire) ne se révèlent qu'après des dizaines d'étapes. De plus, le modèle est limité par sa fenêtre de contexte et son budget de calcul.

Les auteurs résolvent ce problème de façon récursive. L'agent principal lance des agents enfants, et chacun cherche soit une autre stratégie de preuve, soit le lemme nécessaire. Voici comment le dispositif fonctionne :

• chaque enfant dispose d'un contexte vierge et de sa propre copie du projet ; • un enfant peut lui-même engendrer des enfants, et tous les agents ont les mêmes outils ; • un enfant peut consacrer des dizaines d'appels à un seul lemme, mais ne renvoie au parent que le lemme abouti, un contre-exemple ou des résultats partiels ; • les résultats parviennent au parent au tour suivant, sans attendre les autres branches, si bien qu'une découverte précoce peut réorienter la recherche ; • la recherche s'arrête dès que la première preuve valable est acceptée.

L'esprit rappelle la recherche arborescente de Monte-Carlo, mais c'est le modèle lui-même qui décide. Il lit le contenu des réponses de ses enfants et choisit seul quelles branches poursuivre, modifier ou étendre. Le système n'utilise ni compteurs de visites ni estimations moyennes.

Un autre outil est l'essai parallèle de tactiques. L'agent lance plusieurs candidates à la fois sur l'état courant de la preuve. Celle qui fonctionne est réintégrée au contexte, tandis que les traces des tentatives échouées sont écartées, ce qui évite d'encombrer le contexte.

Lean comme service scalable

Les preuves les plus difficiles ont nécessité des dizaines de sous-agents dans un même lancement. Une seule machine n'offrait pas assez de puissance pour Lean : la vérification a donc été déportée dans un service distinct, sans état. Les clients envoient le code source Lean par JSON-RPC au lieu de renvoyer à des fichiers locaux. Toute réplique disponible, pourvu qu'elle utilise les mêmes versions de Lean et de Mathlib, peut traiter n'importe quelle requête.

Chaque réplique contient un pool de processus de travail dans lesquels la bibliothèque Mathlib est préchargée. L'import prend des dizaines de secondes ; les processus sont donc réutilisés, et la vérification sur un processus « chaud » est nettement plus rapide. Les répliques tournent sous Kubernetes, et leur nombre s'ajuste automatiquement à la charge.

Le système est par ailleurs protégé contre la triche. Un agent qui modifie le fichier de preuve pourrait affaiblir l'énoncé du théorème, laisser un `sorry` en guise de bouchon ou ajouter un axiome. Tout ce qui précède la signature du théorème est donc gelé, et la vérification finale revient à Lean Comparator : le fichier doit compiler sans bouchon et n'utiliser que les axiomes autorisés. Le rapport de réussite de l'agent lui-même n'est pas pris en compte.

Un nouvel examen : du code d'olympiade comme tâches de vérification

Les anciens benchmarks sont presque épuisés, et les jeux de vérification de code rédigés à la main restent modestes : ils comptent quelques centaines de tâches, que l'on peut mémoriser ou retrouver dans les données d'entraînement. Les auteurs ont donc construit un pipeline qui génère les tâches automatiquement :

• un agent codeur écrit des solutions sûres en Rust pour des problèmes de type LeetCode, où une fonction pure opère sur des données simples (nombres, listes, chaînes, arbres, listes chaînées) ; • la solution passe des tests de référence, puis est traduite en un modèle exécutable en Lean ; • Rust et Lean sont exécutés sur les mêmes entrées, et seuls les programmes dont les sorties coïncident entièrement sont retenus ; • un agent distinct rédige la spécification, c'est-à-dire une propriété qui doit être vérifiée ou violée ; • l'énoncé est gelé, puis le prouveur le démontre ou le réfute.

Par rapport aux jeux rédigés à la main, ces tâches imposent des obligations au niveau de l'implémentation : arithmétique à largeur fixe, erreurs explicites, boucles générées, conversions de types, remplacement fonctionnel de l'état mutable. Les réfutations fournissent des étiquettes négatives, absentes des pipelines qui ne produisent que des preuves. La spécification est écrite par un autre agent avant que le prouveur ne la voie, et celui-ci ne peut pas choisir une formulation plus facile.

Sur un échantillon d'énoncés, avec une limite de 30 minutes par énoncé, le système n'en résout qu'une partie. Pour un prouveur qui a presque épuisé les anciens benchmarks, ces tâches restent loin de la saturation. On peut les faire passer à l'échelle par le calcul, s'en servir pour comparer d'autres démonstrateurs, et les utiliser comme récompenses dans l'apprentissage par renforcement à récompenses vérifiables (RLVR). Ce test sur du code ne « devine » rien : il produit un verdict vérifiable du noyau. Les mutations de programmes (de petites modifications d'un code correct) fournissent des tâches supplémentaires à étiquettes négatives, mais l'article ne les évalue pas.

Ce que cela change pour les ingénieurs

La principale leçon pratique : sans fine-tuning, on peut miser sur l'infrastructure autour du modèle. L'isolation des contextes, la recherche asynchrone, les essais parallèles et un service de vérification élastique permettent à un modèle ordinaire d'obtenir avec Lean un résultat qui exigeait jusqu'ici des modèles spécialement entraînés, comme Goedel-Code-Prover. Pour ceux qui construisent des agents de vérification de code, le schéma associant énoncé gelé et vérification finale indépendante sera aussi utile : il couvre les moyens les plus courants de tromper le vérificateur.