Des chercheurs de Meta et de l'Université de New York ont conçu un système d'intelligence artificielle épuré pour démontrer des théorèmes mathématiques, qui a égalé ou dépassé des workflows de preuves Lean soigneusement conçus — et ce à un coût moindre.

Ce système, baptisé h1, défend une thèse simple : en démonstration automatique de théorèmes, la simplicité peut l'emporter sur la complexité, à condition que le modèle reçoive un bon retour d'information.

Une boucle agentique minimale

Ces travaux émanent de l'équipe de recherche FAIR de Meta et de l'NYU. Dans un article intitulé « h1 : A Taste of the Bitter Lesson in Automated Theorem Proving », publié le 25 octobre 2026, les chercheurs décrivent h1 comme une boucle agentique minimale qui connecte des grands modèles de langage de pointe à Lean 4 et leur transmet les résultats du vérificateur en temps réel.

Lean 4 est un assistant de preuve open source dans lequel les raisonnements mathématiques sont écrits sous forme de code, de sorte qu'un compilateur — et non un relecteur humain — vérifie chaque étape. Ce dispositif donne au vérificateur le dernier mot : une preuve ne compte qu'une fois compilée.

La plupart des démontreurs automatiques enveloppent le modèle de langage dans un échafaudage élaboré, avec des workflows prédéfinis qui découpent les problèmes, acheminent les sous-tâches et orchestrent de nombreux composants. Le cadre h1 fait l'impasse sur cette machinerie et s'appuie plutôt sur quelques mécanismes simples :

• Édition persistante de fichiers, afin que le modèle travaille sur un fichier de preuve qui conserve son état entre les étapes
• Retour immédiat du compilateur après chaque édition, afin que les erreurs apparaissent sans délai
• Réflexion, en mobilisant la capacité propre du modèle de langage à raisonner sur ce qui a mal tourné

Selon l'article, la performance de h1 provient principalement d'une interface efficace avec Lean, plutôt que d'une orchestration sophistiquée.

Résultats des benchmarks

La recherche indique que h1 a atteint des performances de pointe sur plusieurs benchmarks de démonstration formelle de théorèmes. Sur PutnamBench, un benchmark construit à partir des problèmes de la William Lowell Putnam Competition — le concours annuel de mathématiques destiné aux étudiants de premier cycle nord-américains —, il a obtenu 670 sur 672 avec GPT-5.5. Sur l'évaluation FATE-X, h1 a marqué 90 sur 100.

Le système a également résolu huit problèmes ouverts de la collection FormalConjectures. Il s'agit notamment de variantes des problèmes d'Erdős, un ensemble de questions nommées d'après le prolifique mathématicien Paul Erdős. Comme ces problèmes sont énoncés dans le langage formel de Lean, leur résolution signifie produire des preuves vérifiées par machine plutôt que des arguments rédigés.

La comparaison la plus directe s'effectue avec AlphaProof Nexus de DeepMind. Sur la résolution des problèmes d'Erdős, h1 a affiché un taux de réussite de 82,5 %, contre 76 % pour AlphaProof Nexus. L'écart de coût était plus large que l'écart de précision : h1 a dépensé 121 $ par preuve réussie, contre 317 $ pour AlphaProof Nexus.

La « bitter lesson » appliquée aux mathématiques

Le titre de l'article renvoie à la « bitter lesson » — terme forgé par le chercheur en IA Rich Sutton dans un essai de 2019 pour désigner l'idée selon laquelle les méthodes généralistes et évolutives, adossées à une forte puissance de calcul, tendent à surpasser avec le temps les techniques spécialisées et artisanales.

Ce n'est pas la première incursion de Meta sur ce sujet. Ces travaux s'appuient sur des travaux antérieurs de Meta, dont le démonstrateur de théorèmes neuronal HTPS introduit en 2022, et reflètent un changement d'approche. Les systèmes antérieurs se concentraient sur la construction de recherches plus intelligentes autour du modèle, tandis que h1 mise sur une interaction directe entre le modèle et le vérificateur.

Le facteur temporel compte également. Les résultats de h1 dépendent de modèles de pointe tels que GPT-5.5, et le solide score sur PutnamBench a été obtenu avec ce modèle.

Ce que cela signifie

Les chiffres des coûts constituent l'aspect le plus concret de ces travaux. Une baisse de 317 $ à 121 $ par preuve réussie change la donne quant aux problèmes qu'il vaut la peine de tenter. Lorsque chaque tentative coûte moins cher, les équipes peuvent en mener davantage sur des conjectures plus difficiles ou plus spéculatives. La nature vérifiée par machine des résultats fait aussi partie de l'attrait : les progrès de la démonstration formelle suscitent l'attention bien au-delà des mathématiques, car les assistants de preuve servent également à vérifier des logiciels et des conceptions matérielles.

Certaines réserves s'imposent. Les scores de benchmarks reflètent des performances sur des ensembles de tests spécifiques, et PutnamBench est proche de la saturation avec 670 sur 672 ; la façon dont les systèmes se comportent sur des collections de problèmes ouverts comme FormalConjectures sera donc la mesure la plus intéressante à suivre. L'approche de h1 dépend en outre fortement du modèle de pointe sous-jacent.

Le message plus large de l'article est qu'un modèle de base solide associé à un retour propre du vérificateur peut importer davantage qu'un échafaudage élaboré — un pari qui, sur ces benchmarks, s'est révélé gagnant.

Source : CryptoBriefing