En 24 jours, des agents IA formalisent 15 000 pages de preuves et débusquent une faille

Quelques dizaines d'agents IA ont transformé en 24 jours une démonstration d'environ 15 000 pages en plus de 43 millions de lignes de code, que l'ordinateur vérifie pas à pas. Des mathématiciens de premier plan ont travaillé des décennies sur ce texte, l'une des constructions les plus vastes de l'histoire des mathématiques. En chemin, le système a trouvé dans le raisonnement des auteurs une lacune logique qui existait depuis près de 40 ans.

Une page, trois mille lignes

Formaliser une démonstration revient à écrire explicitement chaque étape que le mathématicien escamote dans son article d'une formule comme « on vérifie sans peine que ». Ensuite, un programme vérificateur doit accepter cette transcription. S'il y a une faille dans l'enchaînement, le code ne passe tout simplement pas la vérification.

L'arithmétique donne la mesure de l'échelle. 43 millions de lignes pour 15 000 pages, cela fait environ 2 900 lignes par page. En 24 jours, cela représente de l'ordre de 1,8 million de lignes par jour, soit environ 75 mille par heure, sans interruption. Une équipe humaine n'aurait pas pu abattre un tel volume : la formalisation de théorèmes même modestes prend généralement des mois à des spécialistes.

Pourquoi c'est une machine qui a trouvé la faille

Cette lacune vieille de près de 40 ans a survécu à des dizaines de lecteurs attentifs. Ce n'est pas une question de négligence de leur part. Vérifier 15 000 pages à la main n'est pas réaliste : le relecteur s'appuie sur l'autorité des auteurs et sur le fait que les étapes intermédiaires sont suffisamment évidentes. Le vérificateur, lui, n'accorde aucun crédit de confiance. Chaque transition, il l'accepte ou la rejette.

La formalisation joue donc aussi le rôle d'audit. L'agent qui tente de coder une étape se heurte à l'endroit où la justification manque. Pour les mathématiques, c'est un signal sérieux : il s'agit de l'intégrité de l'édifice, pas d'une correction cosmétique.

Économie : combien de tokens coûte un tel chantier

Il s'agit d'une estimation de la rédaction, et non de données du projet. À 10-12 tokens par ligne, le code final représente un demi-milliard de tokens en sortie. La consommation réelle est bien plus élevée, car les agents rédigent des brouillons, reçoivent les erreurs du vérificateur, réécrivent et revérifient. Avec ces itérations, le compte se chiffre très probablement en milliards de tokens.

Par ailleurs, le délai de 24 jours a été atteint grâce au parallélisme. Une grande démonstration se décompose naturellement en un graphe de lemmes avec dépendances, et les branches indépendantes peuvent être confiées simultanément à différents agents. Le vérificateur joue ici le rôle d'arbitre avec une réponse binaire, « accepté ou non », si bien que les agents n'ont pas à se croire sur parole.

Chiffres clés du projet :

• environ 15 000 pages de démonstration d'origine, constituée au fil des décennies ;
• 24 jours de travail du système ;
• quelques dizaines d'agents travaillant en parallèle ;
• plus de 43 millions de lignes de code vérifiable ;
• environ 1,8 million de lignes par jour en moyenne ;
• environ 2 900 lignes de code par page de texte ;
• une lacune dans l'argumentation vieille de près de 40 ans.

Ce que l'on peut en retenir pour la pratique d'ingénierie

La principale leçon ne concerne pas seulement les mathématiques. Les systèmes agentiques passent le mieux à l'échelle là où existe un vérificateur automatique sans ambiguïté : compilateur, suite de tests, moteur de preuve. Dans ce cas, des centaines de milliers de lignes générées n'exigent pas de relecture manuelle, car le tri est fait par la machine.

Le même schéma s'applique à la vérification formelle de bibliothèques cryptographiques, de compilateurs, de protocoles de consensus et de blocs matériels. Les conditions sont toujours les mêmes : une spécification détaillée, un vérificateur strict et la possibilité de découper le travail en morceaux indépendants. Pour les équipes qui prévoient des pipelines agentiques, la conclusion pratique est la suivante. Il vaut mieux commencer par investir dans le vérificateur et la décomposition de la tâche ; le nombre d'agents et la taille du modèle passent au second plan. Autre enseignement pour la relecture scientifique : une démonstration formalisée offre une garantie reproductible qu'un texte manuscrit de 15 000 pages ne peut pas donner.