h1 is een onderzoeksopzet waarmee een taalmodel bewijzen ontwikkelt in Lean 4, een omgeving voor het schrijven en controleren van formele wiskundige bewijzen. De auteurs rapporteren sterke scores op verschillende benchmarks, maar die horen bij specifieke modellen en testsets. Ook de opvallende vergelijking met AlphaProof Nexus geldt voor een beperkte groep opgaven, niet voor wiskunde in het algemeen. (de paper over h1)
Hoe h1 met Lean 4 werkt
h1 is een zogeheten harness: een werkomgeving rond een taalmodel, geen op zichzelf staand model. Het model houdt een Lean-bestand bij en past dat in meerdere rondes aan. Lean geeft bij elke aanpassing fouten en nog openstaande bewijsstappen terug. Het model kan daarnaast onder meer zoeken in Mathlib, de wiskundebibliotheek voor Lean, en losse bewijsfragmenten uitproberen. Na een afgewezen inzending vat een reflectiemodel de voortgang en feedback samen voor een volgende poging. De aanpak schrijft geen vaste bewijsopbouw of zoekstrategie voor.
Een bestand dat compileert, is nog niet automatisch een geldig bewijs. SafeVerify controleert de inzending tegen de oorspronkelijke opgave, kijkt of de juiste stellingen zijn gedeclareerd en of alleen toegestane axioma’s zijn gebruikt. Daarna worden de declaraties opnieuw gecontroleerd met de kernel van Lean, het onderdeel dat formele bewijzen verifieert.
Welke resultaten de auteurs rapporteren
Met GPT-5.5 loste h1 volgens de auteurs 670 van de 672 opgaven van PutnamBench op, met één poging per opgave en zonder herhalingen of parallelle pogingen. Met GPT-5.6 Sol rapporteerden ze 90 van de 100 opgaven van FATE-X, een verzameling algebra-opgaven op het niveau van een kwalificatie-examen voor promovendi of hoger; 78 van de 100 opgaven van FC100-solved; 14 van de 23 stellingen van FormalQualBench; en alle zes opgaven van IMO 2026. Dit zijn afzonderlijke tests, geen gezamenlijke score.
De auteurs melden daarnaast acht opgeloste doelen uit 236 doelen die in Formal Conjectures als open waren aangemerkt. Het gaat om varianten van Erdős 138 en Erdős 337, OEIS A108081, A211417 en A022030, Open Quantum Problem 35 en de Written on the Wall II Conjectures 100 en 314. Voor die laatste twee waren de formele stellingen eerst gecorrigeerd. Daardoor zijn die uitkomsten geen bewijs dat de oorspronkelijke formaliseringen ongewijzigd zijn bewezen.
Wat de vergelijking met AlphaProof Nexus meet
De vaak aangehaalde vergelijking betreft vijf Erdős-problemen waarop alle drie de onderzochte systemen minstens één keer succes hadden. Met Gemini 3.1 Pro rapporteerden de auteurs voor h1 een pass@1 van 82,5% en voor AlphaProof Nexus als geheel 76%. Pass@1 is het gerapporteerde slagingspercentage bij één poging.
| Systeem | Pass@1 op vijf Erdős-problemen | Gemiddelde kosten per geslaagd bewijs, voorwaardelijk op succes | Reikwijdte van de kostenraming |
| h1 | 82,5% | US$ 121 | Experimentele, API-equivalente kostenraming |
| AlphaProof Nexus als geheel | 76% | US$ 317 | De raming telt de inferentiekosten van AlphaProof niet mee |
De bedragen zijn experimentele ramingen op basis van tokengebruik en referentietarieven, geen winkelprijzen. Ze zijn bovendien berekend voor geslaagde gevallen. Als ook mislukte pogingen meetellen, bedroegen de gemiddelde uitgaven voor h1 op dezelfde vijf problemen US$ 138 bij pass@1. Voor pass@3 was US$ 202 nodig om minstens 82,5% te halen, met mislukte groepen meegerekend.
De vijf-problemenvergelijking laat Erdős 125 buiten beschouwing: alle 16 h1-replica’s liepen daar vast door een time-out in de Lean-REPL. Over alle zes Erdős-problemen rapporteerden de auteurs andere pass@1-scores: 68,75% voor h1 en 71,67% voor AlphaProof Nexus als geheel. Voor h1 bedroeg pass@3 op die zes problemen 79,73%.
Wat een formeel gecontroleerd bewijs aantoont
Lean en SafeVerify controleren of een bewijs de formele stelling onder de opgegeven regels volgt. Dat zegt op zichzelf niet of die formele stelling de bedoelde informele wiskundige bewering correct weergeeft. De correcties aan de twee Written on the Wall II-stellingen maken dat verschil concreet: de bewijscontrole slaat op de gecorrigeerde formaliseringen.
