Case study: proving sqrt(2) irrational with LPTP and an LLM

Immagina di essere un detective che cerca di risolvere un mistero che ha affascinato gli esseri umani per oltre duemila anni: la radice quadrata di 2 è un numero "razionale"? Nel mondo della matematica, un numero razionale è come una fetta di torta perfetta e pulita (come 3/4 o 5/2). Un numero irrazionale è un decimale disordinato, infinito, che non può mai essere scritto come una semplice frazione. La radice quadrata di 2 è la lunghezza della diagonale di un quadrato con i lati di lunghezza 1, ed è stato dimostrato dagli antichi matematici che è "disordinata": non può essere una frazione.

Ora, immagina di avere due strumenti molto diversi per aiutarti a risolvere il caso. Il primo è un arbitro super-rigido e robotico chiamato LPTP. Parla un linguaggio estremamente preciso e logico (basato su Prolog) e accetterà una prova solo se ogni singolo passaggio è matematicamente perfetto. Se commetti anche un minimo errore, colpirà il martelletto e dirà: "No, invalido". Il secondo strumento è un Large Language Model (LLM), che è come uno studente super intelligente e creativo che ha letto quasi tutto ciò che è stato scritto. Questo studente è bravo a indovinare il passo successivo di una storia o di un problema matematico, ma a volte "allucina", inventando fatti che sembrano corretti ma che in realtà sono sbagliati.

La grande domanda per gli scienziati oggi è: possiamo unire questi due? Possiamo lasciare che lo studente creativo faccia il lavoro pesante di scrivere la dimostrazione, mentre il rigido arbitro controlla ogni singola frase per assicurarsi che lo studente non stia mentendo? Questo articolo esplora esattamente questa partnership, usando l'antico mistero della radice quadrata di 2 come caso di test.

---

La Grande Unione per il Controllo delle Dimostrazioni

In questo articolo, gli autori si sono posti l'obiettivo di vedere se potessero usare un'IA moderna (specificamente, un modello chiamato Claude) per aiutare a dimostrare che la radice quadrata di 2 è irrazionale, ma con un colpo di scena: la dimostrazione doveva essere scritta in un formato molto specifico e rigoroso che l'arbitro robotico (LPTP) potesse comprendere e verificare. Non volevano solo che l'IA dicesse "è vero"; volevano che l'IA scrivesse la reale logica passo dopo passo, che l'arbitro avrebbe poi valutato.

La storia inizia con un'idea semplice. Per dimostrare che la radice quadrata di 2 è irrazionale, di solito si assume il contrario: ovvero che sia una frazione composta da due numeri interi, $p$ e $q$, che non condividono alcun fattore comune (sono "coprimi"). Se si fa il calcolo, si arriva inevitabilmente a una contraddizione in cui entrambi i numeri devono essere pari, il che significa che condividono effettivamente un fattore (2). Questo rompe la regola secondo cui erano coprimi, dimostrando che l'ipotesi originale era errata.

Gli autori hanno cercato di far scrivere all'IA questa dimostrazione nel linguaggio rigoroso di LPTP. All'inizio, l'IA era come uno studente che conosce la storia ma non sa scrivere il saggio nel formato richiesto. Cercava di saltare dei passaggi o di compiere salti logici che l'arbitro non avrebbe accettato.

È qui che avviene il lavoro di squadra. Gli autori hanno impostato un ciclo di feedback:

1. L'IA prova a scrivere un passaggio della dimostrazione.
2. L'arbitro (LPTP) lo controlla.
3. Se l'arbitro trova un errore, indica il punto esatto in cui la logica si è interrotta.
4. Gli autori mostrano questo errore all'IA.
5. L'IA riprova, correggendo l'errore specifico.

Questo processo era simile a un gioco di "caldo e freddo". L'arbitro non diceva solo "sbagliato"; diceva: "Hai commesso un errore nel passaggio 4", permettendo all'IA di correggere la rotta.

I Risultati: Una Vittoria Parziale

L'esperimento è stato un successo, ma con alcune riserve. L'IA è stata in grado di dimostrare autonomamente molti dei pezzi più piccoli e facili del puzzle. Ad esempio, ha dimostrato con successo che "se un numero è pari, il suo quadrato è pari" o che "2 per un numero è pari". Gli autori chiamano queste "lemmi" (piccole dimostrazioni di supporto). L'IA le ha ottenute correttamente, arrivando a volte persino a proporre nuove idee di supporto che gli umani non avevano pensato.

Tuttavia, per la parte più complicata della dimostrazione — la logica specifica che mostra perché la radice quadrata di 2 non può essere una frazione — l'IA si è bloccata. Non riusciva proprio a trovare la strada giusta da sola. Così, gli autori umani hanno dovuto intervenire fornendo all'IA un "indizio" o addirittura scrivendo loro stessi la struttura principale della dimostrazione, chiedendo all'IA di riempire i piccoli spazi vuoti.

Alla fine, hanno prodotto una dimostrazione formale completa che la radice quadrata di 2 è irrazionale. Questa dimostrazione è stata scritta in parte dall'IA e interamente controllata dall'arbitro robotico. L'arbitro le ha assegnato un voto positivo, confermando che la logica era solida.

Cosa Significa Questo

L'articolo non sostiene che l'IA possa ora risolvere tutti i problemi matematici da sola. In effetti, gli autori mostrano esplicitamente che l'IA non può farlo da sola; senza la guida umana e il controllo rigoroso dell'arbitro, l'IA avrebbe probabilmente prodotto una dimostrazione falsa o errata.

Invece, l'articolo suggerisce un nuovo modo di lavorare: l'IA come scrittore di bozze, gli umani come editor e gli strumenti formali come verificatori dei fatti. L'IA è veloce e creativa, genera idee e riempie i dettagli, mentre lo strumento formale (LPTP) agisce come un occhio implacabile che cattura allucinazioni ed errori.

Gli autori hanno anche testato altri strumenti matematici automatizzati (chiamati ATP) per vedere se potessero svolgere il compito più velocemente. Questi strumenti erano veloci e gratuiti, ma producevano dimostrazioni difficili da leggere per gli umani e che non potevano essere facilmente aggiunte alla libreria della matematica verificata. L'approccio dell'IA, pur essendo più lento e richiedendo l'aiuto umano, produceva dimostrazioni leggibili e che potevano essere conservate in sicurezza per uso futuro.

In breve, questo articolo dimostra che non dobbiamo scegliere tra l'intuizione umana e la precisione della macchina. Lasciando che l'IA faccia il lavoro pesante di redazione e che gli strumenti rigorosi facciano il lavoro di valutazione, possiamo costruire un sistema in cui l'IA ci aiuti a dimostrare verità matematiche complesse, purché manteniamo un essere umano nel comando per guidare la nave e un arbitro severo per controllare la mappa. La radice quadrata di 2 rimane irrazionale, ma ora abbiamo un nuovo, collaborativo modo per dimostrarlo.