Ricercatori di Meta e della New York University hanno sviluppato un sistema di intelligenza artificiale essenziale per dimostrare teoremi matematici, che ha eguagliato o superato workflow di dimostrazione Lean meticolosamente ingegnerizzati — e a un costo inferiore.

Il sistema, chiamato h1, avanza un'argomentazione semplice: nella dimostrazione automatica dei teoremi, la semplicità può prevalere sulla complessità, purché il modello riceva un buon feedback.

Un loop agentico minimale

Il lavoro proviene dal team di ricerca FAIR di Meta e dalla NYU. In un articolo intitolato "h1: A Taste of the Bitter Lesson in Automated Theorem Proving", pubblicato il 25 ottobre 2026, i ricercatori descrivono h1 come un loop agentico minimale che collega modelli linguistici di grandi dimensioni di frontiera a Lean 4 e fornisce loro in tempo reale i risultati del verificatore.

Lean 4 è un assistente di dimostrazione open source in cui gli argomenti matematici vengono scritti come codice, quindi è un compilatore, e non un revisore umano, a controllare ogni passaggio. Questa configurazione dà al verificatore l'ultima parola: una dimostrazione vale solo quando compila.

La maggior parte dei dimostratori automatici avvolge il modello linguistico in un'impalcatura elaborata, usando workflow predefiniti che suddividono i problemi in frammenti, instradano i sottocompiti e orchestrano molti componenti. Il framework h1 salta tutta questa macchinaria e si affida invece ad alcuni semplici meccanismi:

• Editing persistente dei file, così il modello lavora su un file di dimostrazione che mantiene il proprio stato tra i passaggi
• Feedback immediato del compilatore dopo ogni modifica, così gli errori emergono subito
• Riflessione, sfruttando la capacità del modello linguistico di ragionare su cosa sia andato storto

Secondo l'articolo, le prestazioni di h1 derivano principalmente da un'interfaccia efficiente con Lean, piuttosto che da un'orchestrazione sofisticata.

Risultati dei benchmark

La ricerca riporta che h1 ha raggiunto prestazioni allo stato dell'arte su diversi benchmark formali di dimostrazione dei teoremi. Sul PutnamBench, un benchmark costruito a partire dai problemi del William Lowell Putnam Competition — la competizione matematica annuale per gli studenti universitari nordamericani — ha ottenuto 670 punti su 672 con GPT-5.5. Nella valutazione FATE-X, h1 ha totalizzato 90 su 100.

Il sistema ha anche risolto otto problemi aperti della collezione FormalConjectures. Questi includono varianti dei problemi di Erdős, un insieme di domande intitolate al prolifico matematico Paul Erdős. Poiché tali problemi sono formulati nel linguaggio formale di Lean, risolverli significa produrre dimostrazioni verificate da macchina anziché argomenti in prosa.

Il confronto più diretto è con AlphaProof Nexus di DeepMind. Sulle risoluzioni dei problemi di Erdős, h1 ha registrato un tasso di successo dell'82,5%, mentre AlphaProof Nexus si è fermato al 76%. Il divario dei costi è stato più ampio di quello di accuratezza: h1 ha speso 121 dollari per dimostrazione riuscita, contro i 317 dollari di AlphaProof Nexus.

La bitter lesson applicata alla matematica

Il titolo dell'articolo richiama la "bitter lesson" — il termine con cui il ricercatore AI Rich Sutton, in un saggio del 2019, indicò l'idea che i metodi scalabili e di uso generale alimentati da calcolo intensivo tendano, col tempo, a superare le tecniche specializzate e artigianali.

Non è il primo tentativo di Meta su questo problema. La ricerca si basa su lavori precedenti di Meta, tra cui il dimostratore neurale di teoremi HTPS introdotto nel 2022, e riflette un cambio di approccio. I sistemi precedenti si concentravano sulla costruzione di ricerche più intelligenti attorno al modello, mentre h1 si concentra nel lasciare che il modello interagisca direttamente con il verificatore.

Anche i tempi contano. I risultati di h1 dipendono da modelli di frontiera come GPT-5.5, e il forte punteggio al PutnamBench è stato ottenuto proprio con quel modello.

Cosa significa

I dati sui costi sono la parte più pratica del lavoro. Un calo da 317 a 121 dollari per dimostrazione riuscita cambia quali problemi valgono la pena di affrontare. Quando ogni tentativo costa meno, i team possono eseguire più tentativi su congetture più difficili o più speculative. La natura verificata da macchina dei risultati è parte dell'interesse: i progressi nella dimostrazione formale attirano attenzione ben oltre la matematica, poiché gli assistenti di dimostrazione sono usati anche per verificare progetti software e hardware.

Alcune avvertenze si applicano. I punteggi dei benchmark mostrano le prestazioni su specifici set di test, e il PutnamBench è vicino alla saturazione con 670 su 672, quindi il modo in cui i sistemi si comporteranno su collezioni di problemi aperti come FormalConjectures sarà la misura più significativa da osservare nei prossimi passi. L'approccio di h1 dipende inoltre in misura notevole dal modello di frontiera sottostante.

Il messaggio più ampio dell'articolo è che un forte modello di base abbinato a un feedback pulito del verificatore può contare più di un'impalcatura elaborata — una scommessa che, su questi benchmark, ha dato i suoi frutti.

Fonte: CryptoBriefing