1 · Canonical rules
One FID engine for legal moves, captures, promotion, and draw state.
PROOFDAMA · PUBLIC PROOF LAB
From finite cases to a universal theorem
ProofDama now follows two auditable paths: the ladder toward the 8×8 solution and a theorem-discovery track over the infinite 2n×3×1 family. Every case must be regenerated, certified, and independently replayed.
Scientific status, without shortcuts
The standard 8×8 initial position with 12 pieces per side is not solved yet. Nine public benchmarks passed the ARM64/x86-64 gate. In the three-row family, the held-out 10×3×1 case is now a verified draw: 46,756,882 canonical positions and 3,787,307,442 FID values replayed on ARM64 and x86-64.
43
historical configurations in the full schema
7,245,724,519
states in the largest historical model
230.1 GB
hash-pinned W/L/D EGDB
9
reduced-geometry certificates
UNIVERSAL THEOREM TRACK · PREREGISTERED CONJECTURE
Not another board: an infinite family
Historical results suggested stabilization after two small exceptions. Before the new computation we froze the conjecture and its falsifiers; 8×3×1 then confirmed the prediction without changing them. Codex is used not only to solve instances, but to extract the invariant that could close an inductive proof.
For every n ≥ 3: WLD(2n×3×1) = draw
ARM64/x86-64 certificates: 2×3×1 = White, 4×3×1 = Black, 6×3×1 = draw, 8×3×1 = draw, and 10×3×1 = draw. The preregistered prediction passed two prospective widths.
The moving-vacancy dualityThe vacancy-first representation matches the canonical engine across 41,701,405 states and 122,287,690 transitions. The first CEGAR cycle examined 164,922,712 deletions and 30,694,340 pairs. The two-ply macro relation also eliminates the roots, despite retaining 4,084,852 White pairs and 3,795,042 Black pairs with no W/L/D contradictions.
The counterexamples reject rigid relations, static controllers and an overly strong boundary-gadget neutrality claim; they do not reject the draw conjecture. An exact recursion from the initial T(n) position to T(n−1) plus a local gadget is now proved. The root-reachable protocol still has to close, so no universal theorem is claimed.
Follow the proof journey →Open the preregistration ↗Read the space-duality note ↗Open the equivalence report ↗Open quotient measurements ↗Open the closure counterexample ↗Open the variable-length audit ↗INDEPENDENT_REPLAY
Certified rung: 2×3×1 = White wins
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
2
certified nodes
1
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 088d78d8d62b13be6a50fa917bbfffbe2c9c9b169b3001f03e37c4ed697378ba
- canonical JSON SHA-256
- e040b85de655a81391516bb7c639ab29afef4aa6830a1b1cb01825c01f116802
- generator commit
- 0d43e1f8241f8c6fd2d383df3dbef460922fabd0
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-2x3x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 4×3×1 = Black wins
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
1,581
certified nodes
2,782
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 15b61a4058e45c49bfb3836186e247d28b74578afb986767cb3bce20e2d59321
- canonical JSON SHA-256
- 4b10550f9709b4a95f5977323a9e7290e1a314538411ed50cab6763108015f0f
- generator commit
- 0d43e1f8241f8c6fd2d383df3dbef460922fabd0
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x3x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 6×3×1 = draw
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
469,144
certified nodes
1,099,413
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 1f0956c9e2deb7050421bd2df457a89d3821498b67fef7a29bf96f72096d93e1
- canonical JSON SHA-256
- 966f3e8e662f103d582449bf7a19964f58f728ee1825d5e2055bcdd3cfea2815
- generator commit
- 0d43e1f8241f8c6fd2d383df3dbef460922fabd0
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-6x3x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 8×3×1 = draw
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
41,230,678
certified nodes
119,611,015
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- e90074bf09542558689626bcb857317a03eb50c698b0def1da25f5f1a61cfd58
- canonical JSON SHA-256
- e90074bf09542558689626bcb857317a03eb50c698b0def1da25f5f1a61cfd58
- generator commit
- 0d43e1f8241f8c6fd2d383df3dbef460922fabd0
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-8x3x1.v1.sharded-manifest.json --adversarialINDEPENDENT_REPLAY
Certified rung: 4×4×1 = draw
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
84,670
certified nodes
172,496
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 5997acfd0baacb1ad76b7a4b26e69f4676603580363c8d0b0908704216a5b4ae
- canonical JSON SHA-256
- a755765ec87be91f0326ae9bf3a810ab4d8702b897540accae056159c79ee449
- generator commit
- dd3e3d8abee3eb5b8f363b08dc1d8881c4aef143
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x4x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 4×6×1 = Black wins
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
1,054,289
certified nodes
2,787,382
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- e6302960b8b7942e38a40346a6daac52dfd757d8ba928cab6587b0dcb0c53e44
- canonical JSON SHA-256
- b822b5024f85581d9c93dda222d1ed5606db97ffb53c038158178ce4d40614a5
- generator commit
- b6ba3363c88d3aaf70deb0060b037945bbdf49f7
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x6x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 6×4×1 = draw
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
27,598,544
certified nodes
77,183,716
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- b4493562df224346cfd4564d6a8c605879a3c006cc5e6c84c80c13d64337c758
- canonical JSON SHA-256
- b4493562df224346cfd4564d6a8c605879a3c006cc5e6c84c80c13d64337c758
- generator commit
- 2c619fef3c540351d018f98122f9bef6b565a405
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-6x4x1.v1.sharded-manifest.json --adversarialINDEPENDENT_REPLAY
Certified rung: 4×8×1 = draw
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
4,617,877
certified nodes
14,125,387
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 14acbaa88de3a6f52729adaca1b3110c33057a62485b1b628e224faeecea0503
- canonical JSON SHA-256
- 0d61ad29ab5ca9c4f07017a55588f9381894cba0ba9d09c1ae537966d65e2739
- generator commit
- fc7fa02a86e3dc3d06c6267801c1cd17fd04cf58
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x8x1.v1.json.zst --adversarialINDEPENDENT_REPLAY
Certified rung: 4×6×2 = Black wins
The canonical engine regenerated the complete reachable graph without consulting the historical database. A separate verifier rebuilt every move and rejected four adversarial mutations.
✓ replayed certificate
191,244,930
certified nodes
519,719,086
replayed transitions
4
corruptions rejected
2
matching architectures
Identical hashes on M4 arm64 and Hetzner x86-64
- compressed artifact SHA-256
- 6ec1c63a4af5cae15980589fc40bf45e7a5924be0dcda4020cf40324d2163258
- canonical JSON SHA-256
- 6ec1c63a4af5cae15980589fc40bf45e7a5924be0dcda4020cf40324d2163258
- generator commit
- a6b058440fb44f665c6572e56da7946da6d92cd3
Replay command
cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x6x2.v1.sharded-manifest.json --adversarialSelected benchmark anchors
Open the full historical schema →| Board | Pieces/side | Result | Model / proof states | Evidence |
|---|---|---|---|---|
| 2x3x1 | 1 | White wins | 2 historical model 2 ProofDama FID | replayed certificate |
| 4x3x1 | 2 | Black wins | 123 historical model 1,581 ProofDama FID | replayed certificate |
| 6x3x1 | 3 | draw | 11,576 historical model 469,144 ProofDama FID | replayed certificate |
| 8x3x1 | 4 | draw | 816,565 historical model 41,230,678 ProofDama FID | replayed certificate |
| 4x4x1 | 2 | draw | 2,836 historical model 84,670 ProofDama FID | replayed certificate |
| 4x6x1 | 2 | Black wins | 26,404 historical model 1,054,289 ProofDama FID | replayed certificate |
| 6x4x1 | 3 | draw | 616,526 historical model 27,598,544 ProofDama FID | replayed certificate |
| 4x8x1 | 2 | draw | 101,023 historical model 4,617,877 ProofDama FID | replayed certificate |
| 6x6x1 | 3 | draw | 15,418,942 historical model | historical retrograde |
| 4x6x2 | 4 | Black wins | 4,167,753 historical model 191,244,930 ProofDama FID | replayed certificate |
| 8x5x1 | 4 | draw | 1,131,369,960 historical model | historical retrograde |
| 8x6x1 | 4 | draw | 7,245,724,519 historical model | historical retrograde |
| 6x9x1 | 3 | draw | 263,390,069 historical model | historical retrograde |
| 8x8x3 | 12 | unknown | — historical model | target |
From measurement to theorem
2 · Enumeration
Retrograde endgame bases and graph-aware df-pn for midgame obligations.
3 · Certificate
The worker emits a versioned artifact with dependencies and data hashes.
4 · Independent replay
A separate verifier replays every obligation and rejects incomplete proofs.
Why can two counts differ?
Legacy play pages sometimes counted records in the player database, while the historical schema counted states in the declared retrograde model. The catalogue now preserves both fields instead of presenting them as one measure.
Next verifiable milestone
The universal track will not build another enormous graph for each wider board. The next gate is a recursive controller restricted to the root-reachable invariant and locally checked against mandatory captures and FID. It must lift both non-losing strategies from T(n) to T(n+1), or emit a precise counterexample.