01
Canonical FID rules
One implementation defines legal moves, maximum captures, king priority, promotion, and the exact draw state.
OPENAI BUILD WEEK · GPT-5.6 + CODEX
Can we prove Italian Checkers?
ProofDama turns a two-decade research project into an auditable proof system: exact Italian rules, pinned endgame data, graph-aware search, portable certificates, and an independent verifier.
Scientific status: the standard 8×8×3 initial position is not solved yet.
UNIVERSAL THEOREM TRACK · ACTIVE
From finite cases to a conjecture over the entire 2n×3×1 family
Codex is not only computing another board: it is helping discover and falsify the invariant needed for induction. The preregistered 8×3×1 prediction is a 41,230,678-state certified draw. After ruling out rigid relations, we implemented a variable-length weak closure with a Büchi objective; the 4×3→6×3 negative control is complete and the true 6×3→8×3 test is active.
43
historical configurations in the full schema
7,245,724,519
states in the 8x6x1 benchmark
230.1 GB
528 pinned EGDB files
9
benchmarks with replayed certificates
WHY THIS IS A DIFFERENT GAME
Italian rules reshape the proof graph
The 2007 result for American checkers does not transfer. Italian Checkers changes capture priority, interactions between men and kings, promotion, and draw semantics. Those rules alter legal edges, cycles, and the obligations a certificate must discharge.
02
Pinned W/L/D data
528 Ed Gilbert EGDB files are identified by manifest and hash before they can support a proof.
03
Graph-aware df-pn
Proof and disproof numbers propagate over shared transposition nodes instead of pretending the state space is a tree.
04
Versioned certificates
Every claim must become a portable artifact containing its root, obligations, dependencies, and statistics.
05
Independent verifier
A separate executable replays every move and obligation. It trusts neither the solver nor this website.
06
Continuous campaigns
A scheduled 12-thread M4 window and a low-priority 24/7 Hetzner worker publish checkpoints, telemetry, and audit logs.
THE RESEARCH STORY
Small solved cases become a proof ladder
Nine certified rungs
Nine benchmarks now have replayed artifacts with matching hashes on M4 arm64 and Hetzner x86-64, including the successful prospective 8×3 test.
Preregistered conjecture
The 2×3 and 4×3 exceptions and stabilization from 6×3 were frozen before 8×3; its 41.2-million-state draw confirms the prediction without rewriting it.
Codex at the meta level
The moving-vacancy engine matches the canonical engine across 41.7 million states. A Büchi product game now searches for variable-length closure: 395,035 states in the negative control, followed by 6×3→8×3.
Active computation
The 6×6 draw is verified on M4 ARM64; an independent replay of its 848.5 million states is running on Hetzner x86-64.
Honest evidence levels
Legacy retrograde results, exact EGDB values, heuristic moves, and verified certificates are never presented as equivalent.
Codex acceleration
GPT-5.6 and Codex helped audit two repositories, remove legacy paths, implement the proof stack, test the rules, and package the research.
The actual finish line
Only an independently replayed root certificate can establish the game-theoretic value of the standard initial position.
A public claim should come with a public test
Explore the benchmark ladder, see what is historical and what is certified, then reproduce the current proof stack locally.