L'enigma dell'alveare ha ora una risposta per ogni dimensione. L'autore ha trovato la dimostrazione con l'aiuto dell'IA, e il programma di verifica Lean l'ha controllata automaticamente; una revisione indipendente è ancora in attesa. Qui viene spiegata senza gergo tecnico, a partire dall'esagono magico.
Un esagono magico è un rompicapo numerico che si gioca su celle a nido d'ape. La dimostrazione che tali esagoni esistono in ogni dimensione è stata trovata con l'aiuto dell'IA e controllata automaticamente da Lean. La dimostrazione automatizzata è costata alcune ore di calcolo. Qui si intende espressamente il rompicapo matematico, non l'omonimo termine della politica economica.
L'articolo spiega prima che cosa richiede il rompicapo e ripercorre la storia dal primo esagono alla dimostrazione. Segue l'idea della dimostrazione in cinque tasselli, ciascuno con una figura. Alla fine ci si chiede perché ci si possa fidare di una dimostrazione verificata dal computer, che cosa deve comunque controllare una persona e quali numeri e fatti stanno dietro al risultato.
Esagono magico: che cosa richiede il rompicapo numerico
La superficie di gioco è una figura a nido d'ape a forma di esagono regolare. La dimensione si chiama ordine n e indica quante celle si trovano su un lato. Un esagono di ordine n è composto da 3n(n−1)+1 celle. Per n = 3 sono 19 celle, per n = 10 già 271.
Nelle celle si scrivono numeri interi, in modo che ogni riga dritta dia la stessa somma. Le righe si contano in tutte e tre le direzioni della figura. In ogni direzione ci sono 2n−1 righe. Le più corte, sul bordo, hanno n celle, quella centrale ne ha 2n−1.
Il più celebre esagono magico contiene i numeri da 1 a 19 e ha ordine 3. Ogni riga dà 38. È l'esagono classico, e partendo da 1 esiste soltanto questa dimensione in cui il rompicapo torna. Una semplice considerazione sulla divisibilità mostra che la somma di riga necessaria è un numero intero solo per n = 1 e n = 3. Per tutti gli altri ordini la variante classica fallisce quindi già in partenza.
Per questo il nuovo lavoro ruota attorno a una variante affine. Invece di partire da 1, si usano i numeri interi da −K a K, ciascuno esattamente una volta. Qui K = 3n(n−1)/2. Per n = 3 sono i numeri da −9 a 9, per n = 10 i numeri da −135 a 135. Ogni riga dà 0 e al centro c'è lo 0.
Il rompicapo sembra innocuo, ma è difficile. Il numero dei possibili riempimenti cresce con n così in fretta che provare al computer non porta lontano. Serviva quindi un piano di costruzione valido per ogni dimensione e una dimostrazione che questo piano funzioni davvero sempre.
Dall'enigma del 1887 al più grande esagono noto: la storia
Il problema originario risale a Ernst von Haselberg e viene solitamente datato al 1887. Alcune fonti indicano il 1888; la fonte primaria non è stata consultata. In seguito Adams ritrovò l'esagono classico, per sua stessa testimonianza nel 1957, e lo rese noto attraverso la rubrica di Martin Gardner. Che questa soluzione sia l'unica, a meno di rotazioni e riflessioni, fu dimostrato da Charles W. Trigg, con pubblicazione nel 1964. Una raccolta in merito è curata dall'Università di Bielefeld, una panoramica è offerta da Wolfram MathWorld.
La variante con numeri interi consecutivi e somma 0 è entrata nel mirino più tardi. Tra il 2004 e il 2006 furono trovati gli ordini da 4 a 8: l'ordine 6 nell'ottobre 2004, gli ordini 7 e 8 nel 2006. Fino al 2006 la soluzione più grande nota era l'ordine 8. Gli ordini più piccoli erano allora già risolti. Una panoramica con i riferimenti è fornita dalla Wikipedia tedesca, le cui date sono in parte prive di fonti.
Nel 2024 Dr. DSGVO, l'autore di questo blog, ha trovato con l'IA una soluzione di ordine 9. All'epoca era la soluzione più grande nota.
Il 2 agosto 2026 Konstantin Gukov ha poi pubblicato sul suo sito New magic hexagons uno schema. Cercava soluzioni fino all'ordine 21 e ha riconosciuto che da esse si può probabilmente ricavare una regola di costruzione per esagoni di qualsiasi grandezza. Gukov ha descritto un algoritmo e uno schizzo di dimostrazione che avrebbe dovuto valere, da ultimo, a partire dall'ordine 114. Egli stesso fa notare che questo schizzo non è formalizzato in Lean né verificato in modo indipendente. La dimostrazione restava quindi ancora da fare.
Per colmare questa lacuna esiste ora una dimostrazione per tutti gli ordini a partire da 3. È nata con l'IA ed è documentata come descrizione del 21 ottobre 2026. Lean l'ha controllata automaticamente, una revisione indipendente è ancora in attesa e i file Lean non sono ancora collegati pubblicamente. Ne riparleremo più avanti.
Tra il primo esagono e la dimostrazione per tutte le dimensioni passano circa 140 anni.
Esagoni magici per ogni dimensione: che cosa è dimostrato
È dimostrato che per ogni ordine n a partire da 3 esiste un esagono magico con i numeri da −K a K, in cui ogni riga, in tutte e tre le direzioni, ha somma 0. È dimostrata anche la versione più forte, in cui inoltre lo 0 sta al centro. Non esiste alcun limite superiore. Lo schizzo di Gukov vale solo a partire dall'ordine 114; gli ordini precedenti restavano aperti senza l'ultimo tassello.
Esistono esagoni magici per ogni dimensione?
La copertura è graduale. L'ordine 2 è impossibile, perché i sette numeri da −3 a 3 non si possono distribuire in modo adatto. Questa parte non fa parte della dimostrazione in Lean. Per gli ordini da 3 a 6 esistono esagoni già pronti, che Lean ha ricontrollato numero per numero. Per gli ordini da 7 a 61 vale un piano di costruzione generale, integrato da una soluzione verificata di un rompicapo parziale per ciascun ordine. Per gli ordini da 62 a 118 vale lo stesso, solo che le liste necessarie sono state ricalcolate e verificate. Dall'ordine 119 in poi basta un piano fisso, dimostrato in generale per ogni n.
Due teoremi principali riassumono il tutto. Il primo afferma che per ogni n a partire da 3 esiste un esagono magico di ordine n. Il secondo dice lo stesso per la versione più forte con lo 0 al centro. Entrambi i teoremi non hanno altra ipotesi che n ≥ 3.
La dimostrazione in cinque tasselli: panoramica
La dimostrazione si può immaginare come una scala. Ogni tassello rimpicciolisce il compito, finché alla fine resta solo una disposizione dei posti su una panchina. I tasselli da 1 a 4 erano già disponibili e verificati. Nuovo è il quinto tassello, la disposizione dei posti per ogni dimensione. È quello che chiude la dimostrazione.
Le sezioni seguenti ripercorrono i tasselli uno dopo l'altro. I primi tre sono intuitivi, gli ultimi due possono essere un po' più tecnici. Tutti i calcoli sono stati verificati da Lean, quindi nel testo bastano le idee.
Tassello 1: ne basta un sesto, perché di fronte sta il negativo
Non occorre pianificare l'intero esagono, ne basta un sesto. Ogni cella ha una cella opposta, situata in posizione speculare rispetto al centro. Se in una cella c'è il numero a, nella cella opposta va −a. Così ogni numero è esaurito insieme al suo negativo, e lo 0 resta per il centro.
Questo ha una conseguenza pratica per le righe. La riga riflessa ha esattamente la somma negativa. Se una riga è equilibrata, lo è anche la sua immagine speculare. Le righe che passano per il centro sono equilibrate addirittura da sole.
Attorno al centro l'esagono si scompone in sei triangoli uguali. Tre di essi sono triangoli di celle opposte: i loro numeri derivano dalla riflessione attraverso il centro con segno invertito. Altri due sono copie del sesto triangolo ruotate di 120 gradi e ricevono numeri strettamente imparentati. Resta un solo triangolo libero con T = n(n−1)/2 celle. Per n = 10 sono 45 invece di 271 celle.
La condizione «ogni riga ha somma 0» diventa così una condizione su questo triangolo. Per ogni riga, una somma pesata dei suoi valori deve dare zero. Questa somma si chiama nel seguito bilancio della riga.
Tassello 2: ogni numero diventa base più cifra
Nel secondo passo ogni numero viene scomposto in due parti, una base e una cifra. Le due parti vengono equilibrate separatamente. Poiché nell'addizione le somme di riga si sommano semplicemente, l'esagono è magico non appena entrambe le parti sono equilibrate da sole.
A tal fine la riserva di numeri da 1 a 3T viene divisa in gruppi di tre: k, T+k e 2T+k per k da 1 a T. Ogni gruppo è la base T+k più T volte una cifra, dove la cifra è −1, 0 o 1. Nell'esagono di ordine 3 si ha T = 3, e la riserva va da 1 a 9. La base 4 dà 1, 4 e 7, la base 5 dà 2, 5 e 8, la base 6 dà 3, 6 e 9.
Il compito si scompone così in due rompicapo indipendenti. Il primo è un campo di cifre formato da −1, 0 e 1 con bilancio zero in ogni riga. Il secondo è un campo di basi, in cui i valori assoluti da T+1 a 2T vengono distribuiti e dotati di segno in modo che il bilancio di ogni riga sia zero.
Tassello 3: il campo delle cifre cresce come una scala
Il campo delle cifre è completamente risolto per ogni ordine a partire da n = 5, e precisamente per induzione a passi di tre. Il principio lo conosce chiunque abbia usato una scala: chi ha il primo piolo e una regola per passare al successivo raggiunge ogni piolo.
Innanzitutto esistono campi di cifre già pronti ed equilibrati per i raggi 4, 5 e 6. Il raggio è qui n−1. Poi vale una regola di ampliamento: un campo di cifre equilibrato si può estendere con tre nuovi strati sul bordo. I nuovi strati hanno un disegno tale che in ogni riga si annullano a vicenda. Da 4 si passa così a 7, 10, 13 e oltre, da 5 a 8, 11 e oltre, da 6 a 9, 12 e oltre. In questo modo si raggiunge ogni raggio a partire da 4.
Questa parte richiede pochissimo tempo di calcolo nella verifica. Risolve però solo il primo dei due rompicapo parziali; il campo delle basi resta aperto.
Tassello 4: distanze desiderate che si compensano a vicenda
Il campo delle basi non viene cercato direttamente. Si stabilisce invece prima, per ogni coppia di celle, di quanto devono differire le sue due basi. Queste distanze desiderate sono dimostrate in generale per tutti gli ordini a partire da n = 13.
Quasi tutte le celle del triangolo formano coppie disposte in modo speculare rispetto al suo asse centrale. Una cella della coppia riceve un meno, l'altra un più. Nel bilancio resta allora solo la differenza dei due valori, mentre la parte comune T scompare. Conta quindi soltanto la distanza tra i due ranghi. Il rango è semplicemente il numero d'ordine: la base T+k ha rango k.
Le distanze desiderate nascono in più passi. Ci sono i cicli di associatività: piccoli schemi di quattro coppie di celle con pesi +1 e −1 e bilancio zero in ogni riga. Il nome deriva dalla regola di calcolo per cui nelle somme le parentesi si possono spostare senza cambiare il risultato. Anche ogni somma di tali schemi ha bilancio zero. Da molti schemi nasce un campo master, in cui nessuna coppia di celle riceve distanza 0. Una distanza 0 sarebbe inutilizzabile, perché due celle non possono mai portare lo stesso numero.
Le celle sull'asse centrale non hanno partner. Ricevono i ranghi più piccoli 1, 2, 3 e così via, e il campo master compensa esattamente il loro contributo. Le celle diagonali portano in più la quota T, che non si annulla. La compensano due catene ramificate di coppie di celle, le foreste. Le loro distanze vengono aumentate di circa T/2, insieme dunque di T.
Il risultato è un insieme completo di distanze desiderate con bilancio zero in ogni riga, nessuna delle quali è zero. La maggior parte delle distanze è piccola e non supera 12. Le celle della prima riga hanno distanze fino a circa 2n, le coppie delle foreste distanze vicine a T/2.
Tassello 5: la disposizione dei posti per ogni dimensione
Infine bisogna distribuire davvero i ranghi da 1 a T in modo che ogni coppia di celle riceva esattamente la sua distanza desiderata. A partire da n = 119 questo avviene con un piano di costruzione fisso, mentre per gli ordini inferiori con liste trovate dal computer e verificate da Lean.
Lo si può immaginare come una disposizione dei posti su una lunga panchina con T posti. Le celle diagonali siedono fisse sui primi posti 1, 2, 3 e così via. Ogni coppia di celle ha bisogno di due posti alla distanza prescritta. Nessun posto può essere occupato due volte. Restano liberi esattamente n−1 posti. Vanno alle celle di bordo senza partner, per le quali ogni posto va bene.
Il trucco decisivo sono i blocchi. Le coppie con la stessa distanza g si possono impilare senza lacune. Con g = 3 le coppie (1, 4), (2, 5) e (3, 6) riempiono i posti da 1 a 6 senza lacune. In generale, g coppie con distanza g riempiono esattamente 2g posti consecutivi, poi segue il blocco successivo. Così ogni gruppo di distanze spreca al massimo g−1 posti alla fine del suo ultimo blocco. I gruppi con distanze da 1 a 12 costano insieme al massimo 0+1+…+11 = 66 posti.
La panchina viene divisa dall'inizio alla fine in cinque zone. Nella prima siede la diagonale. Segue la finestra stellare, in cui una fila speciale di coppie viene annidata come arcobaleni e nelle lacune entrano coppie con distanze 6 e 8. Nella finestra delle foreste siedono coppie con distanze molto grandi, i cui partner finiscono lontano, in un'area riservata. Poi vengono le classi di resto, cioè tutte le altre coppie con distanze da 1 a 12, in blocchi. Per ultime, le n−1 celle di bordo prendono i posti che rimangono.
Perché il piano funziona solo a partire da n = 119? La panchina è quasi esattamente piena. Possono restare liberi solo tanti posti quante sono le celle di bordo senza partner, cioè n−1. Il piano perde al massimo 117 posti: 18 nella finestra stellare, 66 nei blocchi, 21 nella finestra delle foreste e 12 nel salto. Torna quindi appena n−1 è almeno 118. Con n = 119 i posti liberi sono 118 e al massimo 117 vanno persi, quindi rimane un posto di riserva.
Per le dimensioni più piccole un programma ha cercato disposizioni adatte e le ha salvate come liste di numeri. Queste liste si chiamano certificati. Lean ricontrolla ogni certificato da sé, invece di fidarsi del programma di ricerca.
Perché fidarsi della dimostrazione: Lean verifica ogni passo
La dimostrazione non è solo scritta, ma controllata riga per riga da un verificatore. Lean è un linguaggio di programmazione per dimostrazioni matematiche. Ogni deduzione viene scritta con tale precisione che il computer può rifarne il calcolo. Lì non esistono lacune né un «ovviamente». Un errore farebbe interrompere la compilazione.
Si usa inoltre Mathlib, la grande libreria comune di matematica già verificata per Lean, per esempio per le regole di calcolo con insiemi finiti e somme. Nella dimostrazione finita non compare nemmeno un «sorry». Così si chiama in Lean il segnaposto con cui si può saltare provvisoriamente un passo. Non c'è nemmeno un assioma proprio (un'ipotesi di base non dimostrata) né fiducia in codice di programma compilato. Alla fine Lean può elencare su quali ipotesi di base poggia un teorema. Qui sono solo le tre consuete, su cui poggia praticamente l'intera Mathlib: propext, Classical.choice e Quot.sound.
I programmi Python che hanno trovato i certificati e il piano di costruzione non devono essere privi di errori. Un certificato sbagliato o un piano sbagliato verrebbe respinto da Lean. Questo è il vero vantaggio dell'uso di IA e programmi di ricerca: gli strumenti possono tirare a indovinare, la verifica resta comunque rigorosa.
Il computer garantisce che il teorema segue dalle sue definizioni. Se la definizione intende ciò che si intende per esagono magico, deve controllarlo una persona.
Che cosa deve controllare una persona: la definizione in cinque righe
Per ogni dimostrazione verificata dal computer vale un limite: la definizione iniziale non viene controllata, ma presupposta. Nel caso presente la definizione è lunga solo cinque righe e dice, in linguaggio comune, questo: esiste un riempimento delle celle con numeri interi. Nessuna coppia di celle porta lo stesso valore. I valori usati sono esattamente i numeri da −K a K. Ogni riga in ciascuna delle tre direzioni ha somma 0. Nella versione più forte lo 0 sta inoltre al centro.
Tre possibili scappatoie sono escluse. Primo, celle e numeri coincidono: l'esagono ha 3n(n−1)+1 celle, e da −K a K ci sono esattamente altrettanti numeri, quindi «ogni numero esattamente una volta» è imposto. Secondo, i valori fuori dall'alveare non contano, tutte le condizioni riguardano solo celle dentro l'esagono. Terzo, le righe fuori dall'alveare sono vuote, la loro somma è automaticamente 0, il che è innocuo. La formula per K usa la divisione intera, il che non crea problemi, perché n(n−1) è sempre pari.
Durante il controllo è emersa anche una lacuna, nel frattempo chiusa. La definizione originaria non richiedeva esplicitamente lo 0 al centro. La costruzione lo fornisce sempre, perché le celle riflesse portano valori opposti. Ciononostante esiste ora la definizione rafforzata con la condizione aggiuntiva che il centro sia 0, e il secondo teorema principale la dimostra per tutti gli n a partire da 3.
Resta un residuo di fiducia, come in ogni dimostrazione formale. Riguarda il piccolo nucleo di verifica di Lean e le definizioni di base di Mathlib, per esempio per somme e intervalli. È stata usata una versione preliminare di Lean 4. Inoltre la verifica finora è stata eseguita in un solo ambiente. Si sta più sicuri se qualcuno compila i file in modo indipendente sul proprio computer. Facoltativamente un programma di controllo separato come lean4checker può ricontrollare ancora una volta i file di dimostrazione finiti. Per le dimensioni piccole si può inoltre stampare un esagono concreto e ricalcolarlo a mano. Questo non dimostra nulla in più, ma mostra con chiarezza che la definizione coglie ciò che si intende.
Numeri e fatti sulla dimostrazione
Sull'enunciato: è dimostrato un esagono magico con somma zero per ogni ordine n a partire da 3, anche con lo 0 al centro. Esagoni già pronti esistono per n = da 3 a 6. Per n = da 7 a 118 i certificati forniscono la soluzione del rompicapo delle basi; di questi, 57 sono nuovi, cioè quelli per n = da 62 a 118. Il piano di costruzione generale vale a partire da n = 119, che corrisponde al raggio 118. Perde al massimo 117 posti e con n = 119 lascia almeno un posto di riserva. L'ordine massimo dei certificati è n = 118, che corrisponde a 6.903 celle nel triangolo.
Sulle dimensioni: i tasselli da 1 a 4 e i certificati fino a n = 61 sono riuniti in un unico file di 2.713 righe. Il tassello 5 consiste di 40 file con circa 7.000 righe. Il fabbisogno massimo di memoria è di 5,9 gigabyte, per un file relativo alla prima riga del piano. Sono stati usati Lean 4 nella versione preliminare v4.35.0-rc4 e Mathlib. Come assiomi compaiono solo propext, Classical.choice e Quot.sound, lacune aperte non ce ne sono.
Sul tempo di calcolo: la ricostruzione del tassello 5 dura circa 38 minuti, i certificati richiedono in parallelo circa 23 minuti. Alcuni file richiedono molto di più. Il file con i tasselli da 1 a 4 impiega 460 secondi, il file ausiliario con le formule delle distanze desiderate 897 secondi, i certificati per n = da 62 a 89 altri 437 secondi e quelli per n = da 90 a 117 altri 927 secondi. I file della prima riga richiedono insieme circa 18 minuti. Questi tempi descrivono la ricostruzione della verifica finita. L'intera dimostrazione automatizzata, con ricerca e sviluppo, è costata alcune ore.
Sui test preliminari: il piano di costruzione è stato testato numericamente prima della dimostrazione in Lean, come riproduzione esatta delle definizioni per i raggi da 118 a 450. Gli enunciati ausiliari sono stati verificati fino al raggio 20.000. Questi test erano solo un controllo preliminare, la dimostrazione vera e propria è il testo Lean.
Come proseguire: domande aperte e inquadramento
Il lavoro di Gukov e la dimostrazione in Lean si completano a vicenda. Gukov ha fornito lo schema, la costruzione e uno schizzo con il limite 114. Lo schizzo non calcolava le lacune della prima riga e delle foreste. Messe in modo ingenuo, lì sarebbero mancati insieme circa da 2n a 3n posti, più dei consentiti n−1. La dimostrazione in Lean parte proprio da questo punto. Fornisce formule per le distanze desiderate, un piano di impacchettamento con al massimo 117 posti persi invece di 2n–3n e nuovi certificati per gli ordini da 62 a 118. Così sono coperti tutti gli ordini a partire da 3.
Resta per ora aperto il controllo indipendente: una ricostruzione su un computer esterno (già eseguita dall'autore), possibilmente con lean4checker, e una revisione da parte di esperti. I file Lean in questa descrizione non sono ancora collegati pubblicamente. Inoltre Gukov pone sul suo sito una domanda a cui la dimostrazione non risponde: perché i valori delle celle sembrano casuali, mentre i campi di potenziale associati appaiono lisci? Sono immaginabili altre varianti del rompicapo, ma nulla viene promesso al riguardo.
Un rompicapo nato con una figura a nido d'ape di 19 campi è risolto per ogni dimensione. Per questo sono serviti prima l'idea di una persona, poi l'IA come cercatrice e assistente di dimostrazione e infine un verificatore che non crede a nessuno dei partecipanti, ma ricalcola ogni passo.
My name is Klaus Meffert. I have a doctorate in computer science and have been working professionally and practically with information technology for over 30 years. I also work as an expert in IT & data protection. I achieve my results by looking at technology and law. This seems absolutely essential to me when it comes to digital data protection. My company, IT Logic GmbH, also offers consulting and development of optimized and secure AI solutions.
