💻 computer science

The set of primes is supernatural: a Lean formalization of the statement of the conjecture

Questo articolo presenta una formalizzazione completa e verificata da macchina in Lean 4 della congettura secondo cui nessuna funzione non costante costruita mediante identità, costanti e un numero finito di operazioni puntuali (addizione, moltiplicazione, esponenziazione) mappa ogni intero positivo in un numero primo, trasformando così la congettura in un obiettivo preciso e verificabile dal kernel per i sistemi di ragionamento automatizzato.

Autori originali: A. Mayeux

Pubblicato 2026-08-11

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: A. Mayeux

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immaginate una biblioteca vasta e infinita dove ogni libro è un numero. In questa biblioteca, c'è un club molto speciale ed esclusivo chiamato i "Primi". Questi sono numeri che non possono essere costruiti moltiplicando numeri più piccoli; sono gli atomi indivisibili dell'aritmetica, come il 2, il 3, il 5 o il 7. Per secoli, i matematici hanno cercato di scrivere una singola, semplice ricetta — una macchina fatta di strumenti matematici di base — che potesse sputare fuori solo questi membri speciali del club. Volevano una macchina che, qualunque numero le fornissi, producesse sempre un Numero Primo.

Gli strumenti consentiti in questa ricetta sono i più basilari che conosciamo: sommare numeri, moltiplicarli e alzarli a potenze (come elevare al quadrato o al cubo). Potete mescolare e abbinare questi strumenti come preferite, ma non potete usare nulla di sofisticato come la divisione o le radici quadrate. La grande domanda è: esiste un modo per costruire una macchina usando solo questi semplici strumenti che non commetta mai errori? Potrebbe tale macchina generare una lista infinita di primi, o finirà per inciampare e produrre un numero che non è primo? Questo non è solo un gioco; tocca il cuore stesso di come sono strutturati i numeri. Se una tale macchina esistesse, significherebbe che i primi seguono un modello semplice e prevedibile. Altrimenti, significa che i primi sono selvaggi, caotici e "soprannaturali" in un modo che sfida le formule semplici.

Questo articolo è un romanzo investigativo digitale su proprio quesito. L'autore, Arnaud Mayeux, ha preso un particolare articolo matematico che proponeva un'ipotesi audace (una congettura) e ha tradotto l'intero contenuto in un linguaggio informatico chiamato Lean. Pensate a Lean come a un arbitro super rigoroso che controlla ogni singolo passaggio di una dimostrazione matematica per garantire che sia logica al 100%, senza spazio per l'errore umano o per i momenti di "penso che funzioni". L'articolo non risolve il mistero della sorte della macchina generatrice di primi; invece, costruisce un modello digitale perfetto e indistruttibile delle regole del gioco.

Il risultato principale di questo lavoro è che l'intera teoria dietro l'ipotesi della "Macchina dei Primi" è stata codificata con successo nel computer. Ogni definizione, ogni esempio e ogni tabella di numeri dell'articolo originale vive ora all'interno di questo file digitale. L'autore ha controllato 89 diversi esempi di queste "funzioni naturali" (il nome elegante per le macchine costruite con addizione, moltiplicazione e potenze). Per ciascuna di esse, il computer ha calcolato i risultati e ha confermato che tutte alla fine falliscono nel produrre un numero primo. Per esempio, una funzione ha funzionato perfettamente per i primi sei numeri, ma si è rotta al settimo. Il computer ha provato questi fallimenti con assoluta certezza, utilizzando avanzati certificati digitali per verificare numeri enormi che richiederebbero anni di lavoro manuale a un essere umano.

Tuttove, l'articolo è molto chiaro su ciò che non ha fatto. Non ha dimostrato che la Macchina dei Primi sia impossibile. Non ha trovato la risposta definitiva. La congettura centrale — che non esista una tale macchina — rimane un problema aperto, un "problema aperto nominato" nel codice informatico, in attesa che un essere umano o un'intelligenza artificiale riesca finalmente a dimostrarlo. L'articolo dice essenzialmente: "Ecco il regolamento esatto, ed ecco la prova che ogni macchina che abbiamo testato finora fallisce, ma il verdetto finale è ancora pendente".

L'autore ha anche ampliato leggermente il gioco. Ha chiesto: "E se aggiungessimo alcuni strumenti in più, come i fattoriali (moltiplicare un numero per tutti i numeri inferiori ad esso) o le frecce di Knuth (un modo per scrivere potenze enormi)?" Ha costruito una nuova, più ampia classe di macchine con questi strumenti extra e ha enunciato una nuova versione della congettura, ancora più difficile: che anche con questi super-strumenti, non è comunque possibile costruire una macchina che produca solo numeri primi. Questa nuova congettura è anch'essa lasciata aperta, non dimostrata, ma ora è scritta in un modo che un computer può controllare qualora qualcuno dovesse un giorno trovarne la dimostrazione.

In breve, questo articolo è un massiccio atto di traduzione e verifica. Prende un complesso concetto matematico sulla natura caotica dei numeri primi e lo chiude in una cassaforte digitale dove ogni regola è controllata da una macchina. Conferma che, per ogni specifico esempio testato, la "Macchina dei Primi" fallisce, ma lascia la questione ultima — se tale macchina sia teoricamente possibile — come una sfida per il futuro. I primi, sembra, sono davvero "soprannaturali", resistendo a qualsiasi formula semplice con cui cerchiamo di intrappolarli.

Sintesi Tecnica: L'Insieme dei Primi è Soprannaturale: Una Formalizzazione in Lean del Teorema della Congettura

Enunciato del Problema
Il documento affronta la formalizzazione della "Congettura dei Primi Soprannaturali" proposta originariamente in [3]. La congettura postula che nessuna funzione non costante, costruita a partire dalla funzione identità e dalle costanti mediante un numero finito di addizioni, moltiplicazioni ed esponenziazioni puntuali, mappi ogni numero intero positivo in un numero primo. Il documento mira a tradurre questa congettura e il relativo quadro teorico in una formalizzazione verificata da macchina utilizzando Lean 4 e la libreria Mathlib. L'obiettivo è stabilire un target preciso, controllato dal kernel, per la congettura, permettendo sia ai sistemi di ragionamento umano che a quelli automatizzati di tentare una dimostrazione.

Metodologia
La formalizzazione è contenuta interamente in un singolo file Lean 4, SPCL.lean (circa 1200 righe), che dipende esclusivamente da Mathlib. La metodologia consiste in una traduzione diretta ed esaustiva del documento sorgente [3] in Lean, garantendo che ogni definizione, esempio, osservazione, risultato numerato e riga di tabella sperimentale abbia un corrispondente verificato dalla macchina.

Componenti tecniche chiave includono:

Strutture di Elevazione: Il documento axiomatizza le compatibilità di addizione, moltiplicazione ed esponenziazione come una "struttura di elevazione" (una 4-upla $(E, +, \times, \wedge)$ ). Questo è formalizzato come una type class, e la categoria di tali strutture è costruita con leggi di identità e composizione.
Funzioni Naturali: Sono implementate due codifiche equivalenti di "funzioni naturali":
1. Costruzione di Parole: Le funzioni sono generate da parole finite sull'alfabeto $\{A_+, A_\times, A_\wedge\}$ applicate all'insieme delle funzioni identità e costanti.
2. Chiusura Induttiva: Un predicato induttivo IsNatural è definito con costruttori per l'identità, le costanti e le tre operazioni.
  L'equivalenza tra queste due definizioni è formalmente dimostrata.
Formulazione della Congettura: La congettura è enunciata come una proposizione nominata (Conjecture_2_1) di tipo Prop senza una dimostrazione. È esplicitamente definita come un'ipotesi piuttosto che come un assioma o un teorema con sorry, garantendo che la formalizzazione non introduca nuovi assunti.
Verifica Sperimentale: Il documento formalizza 89 risultati sperimentali da [3, §4]. Questi sono enunciati come teoremi che asseriscono la primalità di specifici valori di funzione fino a un certo punto e la compositività del primo valore non primo.
- Per valori più piccoli, le dimostrazioni si basano su norm_num (valutazione computazionale).
- Per valori grandi (ad esempio $2^{2^6} + 93$ ), la formalizzazione utilizza certificati di primalità di Lucas. Questi sono verificati tramite un lemma lucasCert personalizzato che controlla le condizioni $a^{p-1} \equiv 1 \pmod p$ e $a^{(p-1)/q} \not\equiv 1 \pmod p$ per i fattori primi $q$ di $p-1$ , utilizzando il tattico reduce_mod_char di Mathlib.

Contributi Chiave

Formalizzazione Esaustiva: Il documento fornisce una formalizzazione completa e "senza sorry" dell'intero articolo [3]. Ogni definizione, lemma, proposizione e riga di tabella è presente nel codice Lean.
Target di Congettura Preciso: Enunciando la congettura come un Prop nominato e non dimostrato, il lavoro crea un obiettivo specifico e verificabile per i sistemi di ragionamento automatizzato. La struttura delle dipendenze è trasparente; qualsiasi prova della congettura si baserebbe solo sulle definizioni formalizzate e sugli assiomi di Lean/Mathlib.
Estensione Matematica: La formalizzazione estende la teoria di [3, Remark 3.4] definendo una classe più ampia di funzioni, IsNaturalKnuthFactorialSub. Questa classe include:
- La notazione a frecce di Knuth (dove il livello della freccia è esso stesso una funzione nella classe).
- La funzione fattoriale.
- Sottrazione troncata (sotto la condizione $g(n) < f(n)$ ).
  Il documento prova che la classe originale di funzioni naturali si imbedde in questa classe estesa.
Verifica dei Casi Provati: La formalizzazione include prove per i casi in cui la congettura è nota per essere vera (ad esempio, polinomi non costanti, forme lineare-esponenziali e la funzione di Fermat), utilizzando risultati standard della teoria dei numeri tratti da Mathlib (ad esempio, divisibilità polinomiale, Piccolo Teorema di Fermat).

Risultati

Consistenza Formale: Il file SPCL.lean compila in circa 30 secondi. Si basa solo sugli assiomi classici standard di Lean (estensionalità proposizionale, correttezza del quoziente, scelta) ereditati da Mathlib.
Tabelle Sperimentali: Tutti gli 89 righe delle tabelle sperimentali di [3] sono formalizzate come teoremi. Le prove per le affermazioni di primalità per valori grandi sono verificate tramite certificati di Lucas controllati dal kernel, eliminando il rischio di errori di trascrizione nelle stringhe di fattorizzazione.
Equivalenze Teoriche: La formalizzazione prova l'equivalenza tra la formulazione funzionale della congettura e la sua riformulazione insiemistica (ovvero che l'insieme dei primi è "soprannaturale", significando che non contiene un sottoinsieme naturale infinito).
Conseguenze: Condizionatamente alla congettura, la formalizzazione prova che l'insieme dei numeri di Fermat composti è infinito e che l'insieme dei valori non primi per qualsiasi funzione naturale non costante è infinito.

Significatività
Il documento afferma che la sua principale significatività risiede nel rigore e nella completezza della formalizzazione. Trasforma una "sfida difficile per qualsiasi tipo di intelligenza" (come descritto in [3]) in un target preciso e verificabile da macchina. Rimuovendo ogni ambiguità e assicurando che ogni passaggio sia controllato dal kernel di Lean, il lavoro permette ai sistemi di ragionamento automatizzato di tentare una dimostrazione della congettura senza il rischio di errori umani nelle definizioni sottostanti. Il documento non pretende di risolvere la congettura, ma piuttosto di fornire l'infrastruttura necessaria affinché una tale soluzione possa essere validata. Dimostra inoltre la fattibilità della formalizzazione di congetture di teoria dei numeri complesse e guidate sperimentalmente all'interno dell'ecosistema Mathlib.

Articoli simili