ProofDama: Certifying Italian Checkers

An open, continuous proof campaign for Italian Checkers: parallel workers turn contributed compute into independently replayable certificates under the real Italian rules.

Comment

ProofDama: from 640 KB of memory to a mathematical proof

Inspiration

This project began almost forty years before GPT-5.6 existed.

I started playing chess as a child. At eight, I was winning tournaments; at eleven, my play was mentioned by the Italian champion in issue no. 11 of TuttoScacchi. Games were already more than entertainment to me: they were small universes governed by exact rules, strategy, memory, and computation.

At twenty-three, while studying Engineering, I proposed a chess-playing program for my Information Structures exam. The available time was short, so halfway through the project I switched from chess to Italian Checkers. I was not an expert checkers player, which led me to an unusual solution: I made the program play against itself and retain the strategies that performed better.

It became a primitive self-play evolutionary experiment—something resembling a genetic program, although I did not describe it that way at the time. The program improved until it could defeat me. During the exam, it also defeated my professor, who awarded me the highest grade.

It was written in Lisp and ran on an Intel 80286 with an 80287 coprocessor and 640 KB of RAM.

Almost four decades later, in what the Italian philosopher Giambattista Vico might have called a ricorso—a return to an old beginning—I came back to checkers. This time, the objective was far more ambitious: not merely to write a program that played well, but to pursue a weak mathematical solution of Italian Checkers, as Jonathan Schaeffer and his team achieved for English/American checkers.

A weak solution determines the game-theoretic result of the initial position under perfect play. It must establish whether White can force a win, Black can force a win, or both can force at least a draw.

I contacted Ed Gilbert, whose work on checkers endgame databases is internationally respected. He shared his Italian endgame material covering positions with up to ten pieces and discussed his algorithms and data formats with me. His original tooling was primarily written in C++ for Windows. Because I prefer Linux, macOS, portable systems software, and explicit memory control, I began building a new implementation in Rust.

The first version produced a strong playable engine, but the project eventually stalled. The difficulty was not just computation. It was maintenance, distributed execution, and—most importantly—turning a result into something that could genuinely be called a mathematical proof.

Months later, I decided to revisit this seemingly impossible project with GPT-5.6 in Codex.

That changed its trajectory.

What it does

ProofDama is a proof-engineering platform and a continuous research campaign for solving Italian Checkers under the official Italian rules.

It deliberately separates three very different concepts:

  1. a program that plays strongly;
  2. a search process that reports a result;
  3. an independently replayable mathematical certificate.

Only the third is considered proof.

The public website offers a playable Italian Checkers engine, an English project presentation, a live research dashboard, and a Proof Lab showing the progression from reduced geometries to the full 8×8 game.

The scientific system underneath it includes:

  • a canonical Rust implementation of the Italian rules;
  • graph-aware, resumable depth-first proof-number search;
  • deterministic parallel graph construction;
  • Ed Gilbert WLD and MTC endgame evidence;
  • content-addressed artifacts and SHA-256 manifests;
  • a transactional coordinator for multiple workers;
  • atomic checkpoints that survive interruption;
  • and independent verifiers that regenerate every legal move instead of trusting the solver.

The standard 8×8 initial position is not solved yet. ProofDama is an honest, continuously progressing campaign toward that result.

To validate the complete method before attempting the enormous standard game, I use reduced boards as a scientific evidence ladder. These are not merely visual demonstrations: they exercise the same essential requirements—complete state enumeration, cycles, exact rules, deterministic parallelism, certificate production, independent replay, corruption rejection, and cross-architecture reproducibility.

For a draw at the root, ProofDama must independently establish both obligations:

$$ \neg(\text{White can force a win}) \land \neg(\text{Black can force a win}). $$

A search score is not enough. Both claims must be closed by replayable evidence.

How we built it

ProofDama combines a trusted proof core with an untrusted discovery layer.

The canonical state identity is:

$$ (\text{board},\ \text{side to move},\ \text{FID endgame counter in plies}). $$

The third component is essential. Italian Checkers has a formal endgame-count procedure: when the conditions of Article 10 apply, a draw is reached after forty moves made with kings by each player, represented internally as eighty plies. A move by an ordinary piece or a change in the number of pieces resets the count.

This means that two visually identical boards can represent different proof states. A transposition table indexed only by board and side to move would be mathematically unsound.

Italian Checkers also has unusually strict capture rules. Capturing is mandatory, but choosing a capture is not simply a matter of taking the largest number of pieces. The official rules impose an ordered hierarchy involving the number and type of pieces captured, the type of capturing piece, and the order in which opposing pieces are encountered.

Ordinary pieces can capture only forward and cannot capture kings (promoted pieces). During a multiple capture, captured pieces are removed only after the complete move has ended. If an ordinary piece reaches the promotion row during a capture, that move ends immediately.

The architecture contains several distinct layers:

  • Canonical Rust rules engine: generates legal moves and exact state transitions under the frozen FID interpretation.
  • Graph-aware df-pn worker: searches Boolean win and disproof obligations while sharing exact transpositions.
  • Deterministic parallel builder: distributes frontier batches across CPU cores, then globally reorders states so the final certificate does not depend on thread scheduling.
  • WLD/MTC endgame adapter: reads manifest-pinned Gilbert data while preserving the distinction between a database result and an official FID proof.
  • Durable coordinator: manages transactional leases, worker heartbeats, immutable artifacts, resumable jobs, and a hash-chained event history.
  • Independent verifier: reconstructs legal moves and checks every state transition, universal reply, rank, hash, and oracle reference.
  • Bilingual public product: a Next.js website aligns the playable game, scientific status, evidence ladder, and continuous campaign.

The computation is deliberately hybrid. My Apple Silicon M4 Max contributes scheduled high-performance runs using up to twelve worker threads and 64 GB of unified memory. A 32 GB Hetzner Linux server handles compatible low-priority jobs, coordination, telemetry, and continuous operation.

Every job declares its memory requirements. The Hetzner worker automatically refuses workloads that do not fit safely, while continuing smaller compatible jobs and protecting the public services running on the same machine.

Each machine produces versioned artifacts that must pass independent verification. Hardware is never trusted merely because it completed a job.

How GPT-5.6 and Codex were used

GPT-5.6 in Codex became my engineering and proof-audit collaborator.

I used it to inspect both the backend and frontend repositories, identify duplicated and obsolete implementations, remove legacy paths, normalize the architecture, reason through FID rule semantics, implement Rust and Python proof components, create adversarial tests, operate resumable jobs on the remote server, and align the public website with the actual scientific evidence.

Codex was particularly effective in three areas.

First, it could understand and audit the repository as a system rather than edit isolated files. It helped reduce hundreds of historical experiments to one supported proof path.

Second, it could develop across boundaries: Rust state identity, proof schemas, Python coordination, deterministic parallelism, database formats, frontend claims, deployment, and independent verification all had to remain consistent.

Third, it supported the scientific and submission process itself: technical documentation, cost and feasibility analysis, public storytelling, media, reproducible judge instructions, and continuous live validation.

One concrete example came from the 230.1 GB endgame archive. A first checksum inventory appeared healthy, but structural analysis found a missing index partner. Codex helped identify the inconsistency, verify the corresponding data, add a permanent structure audit, rebuild the 528-file manifest, and complete a second full rehash of all 230,121,148,655 bytes.

I retained the decisive research responsibility. I chose to pursue a weak solution instead of presenting a strong bot as “solved”; froze the rule interpretation; excluded heuristic evaluations from the trusted proof base; required independent replay; and established the central rule of the project:

Unfinished work must never be described as certified.

Challenges we ran into

The rules are part of the theorem

A proof of the wrong game is not a proof. Small misunderstandings in capture priority, promotion, delayed removal of captured pieces, or the endgame counter can change the graph being solved.

State-space explosion

The official endgame counter expands the state identity beyond the visible board. The full game requires managing billions of exact states, millions of transitions per second, and data measured in hundreds of gigabytes.

A result is not a certificate

Minimax, opening books, heuristics, and endgame probes can produce excellent moves, but none can be accepted blindly. The independent verifier must reject omitted replies, illegal transitions, incorrect counters, invalid ranks, broken hashes, and unsupported oracle claims.

WLD is not automatically an official FID win

A win/draw/loss tablebase result does not necessarily prove that a win is achieved within the official move-count procedure. ProofDama therefore distinguishes WLD evidence from MTC-linked forward evidence and from a fully certified result.

Cycles and transpositions

Game graphs contain cycles and repeated positions. Treating every repeated state as a draw would be unsound, while treating the graph as a tree would cause enormous duplication. The proof system must share exact states without losing the logical meaning of OR and AND obligations.

Parallelism must remain deterministic

A conventional concurrent hash table can produce node identifiers based on thread timing. ProofDama instead discards completion order, sorts exact state keys before admission, and performs a canonical global reindex.

Runs with one thread, twelve threads, and resumed checkpoints can therefore produce identical certificate bytes.

Real hardware has limits

A 6×4×1 attempt on the 32 GB Hetzner server approached the Linux out-of-memory boundary after discovering millions of states. Instead of hiding the failure, ProofDama converted it into a measured admission rule: this job now requires at least 40 GiB of memory.

The Hetzner worker therefore refuses 6×4×1 while continuing compatible work. This protects both the scientific artifacts and the public services.

Accomplishments that we're proud of

During Build Week, ProofDama moved from a difficult historical solver project to a versioned proof platform.

The most important completed results are:

  • 4×4×1: certified draw over 84,670 exact states;
  • 4×6×1: certified Black win over 1,054,289 exact states;
  • 4×8×1: certified draw over 4,617,877 states and 14,125,387 legal edges.

All three certificate artifacts were reproduced byte-for-byte on Apple Silicon ARM64 and Hetzner x86-64. Independent verifiers accepted them, while deliberately corrupted variants were rejected.

Additional accomplishments include:

  • a canonical, frozen Italian rules surface;
  • graph-aware and resumable df-pn search;
  • deterministic multi-core construction producing identical results with one and twelve threads;
  • atomic resume across different thread counts and batch sizes;
  • independent proof and obligation-certificate verifiers;
  • WLD/MTC evidence bound to versioned SHA-256 manifests;
  • a verified archive of 528 endgame files and 230.1 GB, hashed twice;
  • a durable SQLite coordinator with leases, immutable artifacts, WAL transactions, and a hash-chained event ledger;
  • automated tests covering valid proofs and adversarial mutations;
  • and a public evidence ladder that distinguishes historical results, independently replayed certificates, active work, and unsolved targets.

The next rung, 6×4×1, has already completed deterministic discovery and evaluation of 27,598,544 exact states on the M4 Max.

The complete graph is stored in a compressed checkpoint, including its states, edges, values, and ranks. The Mac is now canonically ordering those states and streaming the final compressed certificate to disk. It is not repeating the graph discovery.

Until certificate generation and independent replay are complete, this remains a measured milestone—not a fourth certified result.

What we learned

The greatest lesson is that solver engineering and proof engineering are different disciplines.

A fast answer is not a proof.
A checksum list is not a completeness proof.
A cycle is not automatically a draw.
A tablebase win is not automatically a rules-compliant win.
A worker reporting “completed” is not independent verification.

I also learned how powerful an AI coding agent can be when it is used not only for speed, but for consistency and epistemic discipline.

GPT-5.6 did not replace the human research decisions. It made it possible to propagate those decisions coherently across code, tests, data, operations, documentation, and the public product. It repeatedly transformed discovered failure modes into permanent automated checks.

On a personal level, the project connected two distant moments of my life: a Lisp program learning through self-play on a 640 KB machine, and a distributed, independently verifiable Rust proof campaign built with Codex nearly forty years later.

What's next for ProofDama: Certifying Italian Checkers

The immediate milestone is to finish streaming and independently replaying the 6×4×1 certificate on my 64 GB ARM64 M4 Max.

Its complete graph of 27,598,544 states is already safely checkpointed, so the search does not need to be repeated. Cross-architecture reproduction will follow on a machine with at least 40 GiB of memory. The 32 GB Hetzner server correctly refuses this job while continuing smaller compatible work.

After that, the reduced-board ladder will advance through progressively larger geometries. Each new rung will measure memory, storage, throughput, certificate size, and replay cost before the next one is admitted.

For the standard 8×8 game, the major engineering gates are persistent disk-scale graph storage, complete forward MTC conversion evidence, measured decomposition of the opening branches, and independent clean-machine replay of the final root certificate.

ProofDama is designed as a continuous, community-oriented research campaign. Contributors can provide:

  • independent certificate replay;
  • code and rules review;
  • CPU, RAM, or storage from compatible machines;
  • new versioned workers;
  • or transparent funding dedicated to compute and artifact publication.

The finish line is intentionally demanding: every opening branch closed, the root certificate replayed from scratch on an independent system, and the ruleset, source commit, schemas, database manifest, commands, logs, and final hashes published together.

Only then will ProofDama say:

Italian Checkers is certified.

Built With

Share this project:

Updates