A PROOF IN THE MAKING · 2n×3×1
ProofDama is not merely trying increasingly larger boards. It is turning finite results into a possible proof for an infinite family, while preserving failed experiments as verifiable counterexamples.
The conjecture is supported by three consecutive certified cases — 6×3×1, 8×3×1 and 10×3×1 are draws — and now has an exact recursive lemma. The inductive closure needed to turn those facts into a theorem for every n ≥ 3 is still open.
Preregistered conjecture
For every n ≥ 3: WLD(2n×3×1) = draw
Each stage is classified, not reinterpreted after the fact.
The canonical engine includes mandatory-capture priority, promotion, temporarily blocking captured pieces and the exact FID draw counter. The conjecture, small exceptions and falsifiers were frozen before the prospective test.
A prediction changed after computation is not a prediction.
2×3×1 and 4×3×1 are the initial exceptions. 6×3×1, 8×3×1 and the held-out 10×3×1 case are draws. For 10×3, the verifier regenerated 46,756,882 canonical positions, 144,871,268 edges and 3,787,307,442 FID values on ARM64 and x86-64.
Many matching cases are strong evidence, but not a universal proof.
The vacancy-first representation describes play through empty cells without losing colour, piece type, turn, promotion, temporary blockers or FID state. It was exhaustively compared with the canonical engine on certified cases.
The dual view exposes the frontier that must remain invariant when two columns are added.
Neutral insertions, fixed-radius relations, two-ply macro moves, static geometric controllers and several finite projections do not close the root. Every failure preserves its first counterexample and narrows the next relation class.
A certified negative experiment prevents an elegant but false proof from being published.
After White’s legal boundary move, T(n) contains an exact copy of T(n−1) with Black to move, plus the local gadget “Black man, White man, vacancy”. The new intrusion has one legal response: a mandatory capture that promotes and ends the sequence.
Width no longer has to be enumerated; it can become recursion depth.
We must show that the root-reachable recursive protocol gives both colours a non-losing strategy at every depth while respecting capture priority and the FID counter. Gadget neutrality over every possible position is false; the narrower property over the reachable invariant is both necessary and sufficient.
The theorem will come from closing the invariant, not from another large database.
THE TURNING POINT
Before: solve T(n), then build and solve T(n+1). Cost grows with the complete graph.
Now: verify all local transitions of the boundary gadget once and prove that a strategy for T(n) lifts to T(n+1).
Codex orchestrates the conjecture → generator → counterexample → refinement → verifier loop. It does not decree a proposition true: it produces code, tests, artifacts and explanations that make each step inspectable and repeatable.
A COST-CONTROLLED CLOSURE PLAN
No more wide enumeration. The only target is the inductive lifting of both non-losing strategies from n to n+1.
The symbolic state contains gadget phase, capture priority, FID class and a stack of dormant modules; it does not contain the whole board.
The canonical engine enumerates every frontier-window configuration. Each transition must remain inside the invariant, decrease a well-founded measure, or emit a counterexample.
The verifier regenerates moves without trusting synthesizer IDs. The output is a small local certificate, cheap to replay on ARM64 and x86-64.
Certified base T(3). Inductive step for both colours. FID termination lemma. Only after all three may the page say “theorem”.
Proposed discipline: short cycles with one hypothesis, one automatic local test and immediate stop at the first counterexample. Tokens are used to formulate and review lemmas; the Mac runs finite enumerations. No continuous conversational monitoring and no new graphs with hundreds of millions of states.
Code, deterministic reports and falsifiers are versioned. The reference commit preserves failed attempts too, because they are part of the scientific record.