h1 et les preuves formelles : ce que mesurent ses résultats

h1 est un dispositif qui permet à un modèle de construire des preuves mathématiques dans Lean 4, un environnement où le code de preuve est vérifié formellement. Ses auteurs rapportent de bons résultats sur plusieurs benchmarks, mais chaque score dépend du modèle et du jeu de problèmes testés. Leur étude sur h1 détaille aussi une comparaison de coûts avec AlphaProof Nexus qui porte sur cinq problèmes d’Erdős.

Comment h1 construit une preuve dans Lean 4

h1 n’est pas un modèle unique : c’est une interface de travail autour d’un modèle de langage et de Lean 4. Le modèle modifie un fichier de preuve conservé d’un tour à l’autre. Après chaque modification, Lean renvoie les erreurs et les objectifs mathématiques qui restent à résoudre. Le modèle peut aussi chercher des définitions et des lemmes dans Mathlib, la bibliothèque mathématique utilisée avec Lean, ou vérifier une idée dans l’environnement d’exécution.

Si une soumission échoue, un modèle de réflexion résume les progrès et les retours du vérificateur pour guider une nouvelle tentative. Les auteurs ne prescrivent pas de plan de preuve ni de méthode de recherche particulière : le modèle choisit comment utiliser les outils disponibles.

Des scores liés à chaque modèle et à chaque benchmark

Avec GPT-5.5, les auteurs rapportent 670 problèmes résolus sur 672 dans PutnamBench, en une tentative par problème, sans répétition ni parallélisme. Avec GPT-5.6 Sol, ils rapportent 90 sur 100 dans FATE-X, un ensemble de problèmes d’algèbre de niveau examen de qualification doctorale ou supérieur, ainsi que 78 sur 100 dans FC100-solved, 14 sur 23 dans FormalQualBench et 6 sur 6 pour les problèmes de l’IMO 2026. Ces résultats proviennent de benchmarks distincts et ne forment pas un score général de capacité mathématique.

Le papier rapporte également huit cibles résolues parmi 236 considérées comme ouvertes dans Formal Conjectures : des variantes des problèmes d’Erdős 138 et 337, les entrées OEIS A108081, A211417 et A022030, Open Quantum Problem 35, et les conjectures 100 et 314 de Written on the Wall II. Les auteurs précisent que ces deux dernières ont été démontrées après correction de leurs énoncés formalisés.

Ce que compare le chiffre face à AlphaProof Nexus

La comparaison mise en avant porte sur cinq problèmes d’Erdős et utilise Gemini 3.1 Pro. Sur cet ensemble, le taux pass@1, c’est-à-dire le taux de réussite après une tentative, atteint 82,5 % pour h1 et 76 % pour le système complet AlphaProof Nexus.

Ces moyennes conditionnelles ne comptent pas les tentatives infructueuses. Sur les mêmes cinq problèmes, la dépense moyenne de h1 atteint 138 $US lorsque les échecs sont inclus. Avec trois tentatives, elle atteint 202 $US pour un taux de réussite d’au moins 82,5 %. Les auteurs calculent ces coûts expérimentaux à partir des jetons utilisés et de tarifs de référence : ce ne sont pas des prix commerciaux.

Le sous-ensemble de cinq problèmes écarte Erdős 125, pour lequel les 16 répliques de h1 se sont terminées par un délai d’attente dépassé dans Lean. Sur l’ensemble des six problèmes, les taux pass@1 rapportés sont de 68,75 % pour h1 et 71,67 % pour AlphaProof Nexus complet; celui de h1 passe à 79,73 % en pass@3. Ces chiffres répondent à un périmètre différent de la comparaison à cinq problèmes.

Ce qu’une preuve formelle vérifie

La compilation ne suffit pas à valider une preuve. SafeVerify compare la soumission à l’énoncé immuable du problème, contrôle les déclarations visées et les axiomes autorisés, puis Lean rejoue les déclarations dans son noyau, la partie qui vérifie les preuves formelles.

Cette vérification établit qu’une preuve respecte l’énoncé formalisé et l’environnement de preuve utilisés. Elle ne garantit pas, à elle seule, que cet énoncé traduit fidèlement la conjecture informelle visée. Les corrections apportées aux énoncés de deux cibles de Written on the Wall II illustrent cette différence.