01
Regole FID canoniche
Presa obbligatoria e massima, priorità della dama, divieto pedina→dama, promozione e stato esatto dell’Art. 10.
PROOFDAMA · RICERCA APERTA E VERIFICABILE
Dimostrare la Dama Italiana
Non basta un’AI forte. Per risolvere il gioco standard 8×8 serve una catena completa: regole italiane esatte, dati identificabili, ricerca esaustiva, certificati portabili e verifica indipendente.
Stato scientifico: la posizione iniziale 8×8×3 non è ancora risolta.
UNIVERSAL THEOREM TRACK · ATTIVA
Da casi finiti a una congettura sull’intera famiglia 2n×3×1
Codex non calcola soltanto un’altra scacchiera: aiuta a scoprire e falsificare l’invariante necessario all’induzione. La previsione preregistrata 8×3×1 è una patta certificata su 41.230.678 stati. Dopo aver escluso le relazioni rigide, abbiamo implementato una chiusura debole a lunghezza variabile con obiettivo Büchi; il controllo negativo 4×3→6×3 è concluso e il vero test 6×3→8×3 è attivo.
43
configurazioni storiche nello schema completo
7.245.724.519
stati nel benchmark 8x6x1
230,1 GB
528 file EGDB bloccati
9
benchmark certificati e rigiocati
PERCHÉ È UN ALTRO PROBLEMA
Le regole cambiano il grafo della prova
Il risultato ottenuto per la dama americana non si trasferisce alla variante italiana. Le priorità di cattura, le restrizioni fra pedine e dame, la promozione e la regola di patta definiscono mosse e cicli differenti. Una prova corretta deve incorporare questi vincoli in ogni nodo.
02
EGDB W/L/D bloccati
528 file e 230,1 GB identificati da manifest e hash: nessun dato esterno entra nella prova senza provenienza.
03
df-pn graph-aware
Il worker riusa i transposition node e propaga proof/disproof numbers sul grafo, non su un albero fittizio.
04
Certificati versionati
Ogni conclusione deve diventare un artefatto portabile, con root, obbligazioni, dipendenze e statistiche.
05
Verificatore indipendente
Un programma separato rigioca mosse e obbligazioni: non deve fidarsi né del solver né del sito web.
06
Campagna continua
M4 con finestra schedulata a 12 thread e Hetzner h24 a bassa priorità, con checkpoint, telemetria e log verificabili.
DAL 2004 A OGGI
I risultati minori diventano il banco di prova
Scacchiere ridotte
43 configurazioni storiche, da 4×4 fino ai modelli da miliardi di stati, forniscono target concreti.
Catalogo canonico
Un file versionato conserva geometria, risultato, stati del modello, record del player e livello di evidenza.
Nove gradini certificati
Nove benchmark hanno artefatti rigiocati con hash concordi su M4 arm64 e Hetzner x86-64, compreso il test prospettico 8×3.
Congettura preregistrata
Le eccezioni 2×3 e 4×3 e la stabilizzazione da 6×3 erano congelate prima di 8×3; la patta su 41,2 milioni di stati conferma la previsione senza riscriverla.
Codex al meta-livello
Il motore duale coincide con quello canonico su 41,7 milioni di stati. Ora un gioco prodotto con obiettivo Büchi cerca una chiusura a lunghezza variabile: 395.035 stati nel controllo negativo, poi 6×3→8×3.
Calcolo attivo
Il 6×6 è una patta verificata su M4 ARM64; il replay indipendente dei suoi 848,5 milioni di stati è in corso su Hetzner x86-64.
Obiettivo 8×8×3
Solo una catena integralmente verificata potrà sostenere il risultato teorico della posizione iniziale standard.
Segui una dimostrazione che si può controllare
Numeri, limiti e passaggi aperti sono pubblicati insieme. Il sito non chiama “risolto” ciò che non possiede ancora un certificato verificato.