The counterexample
Domineering is a partizan placement game: Left places vertical dominoes and
Right places horizontal dominoes on a finite region. A long-standing
conjecture attributed to Berlekamp asserted that every finite Domineering
position has temperature at most 2.
Lech Mazur's manuscript gives an exact counterexample. Lean checks the
board–target game equivalence, the explicit target's thermograph, the complete
30-move rectangle replay, and the resulting existential theorem through the
development's narrow value-and-temperature witness. The stronger witness is
a 28-cell position B' reached by an explicit alternating sequence of 30
legal moves from an 11 × 8 rectangle. Its exact game is
G(B') = { 17/8 | -2 + * },
so, in the nonnegative-temperature convention used in the paper,
t(G(B')) = 33/16 = 2.0625 > 2, with mean1/16.
The Berlekamp collaboration page retains the broader research frontier and open follow-up tasks.
What the infographic shows
The infographic displays the actual 11 × 8 replay. Odd-numbered cyan
dominoes are Left's 15 vertical moves; even-numbered coral dominoes are
Right's 15 horizontal moves. The white cells and two gold cells are exactly
the 28 cells left after move 30. Thus the graphic shows the moves as well as
the final position; the coordinate table in the paper and Lean theorem are
the certificates.
The 26-cell core and the repair
The connected 26-cell core B has the same exact value, but it has
checkerboard imbalance 14 − 12 = 2. A rectangular board has imbalance at
most one, while every played domino removes one cell of each color. Therefore
B cannot itself occur as the remainder of play from any rectangle.
The repaired position translates B two cells to the right and adds the
single cells (0,1) and (1,4). Both are isolated from every other remaining
cell, so neither player can cover either one with a domino. Each is a zero
component, and consequently
G(B') = G(B) + 0 + 0 = G(B).
The explicit 30-move replay proves the stronger rectangle-reachable statement.
Lean-checked scope
The frozen Lean source is identified by commit
9edd1d307a62bcd1b59c4450c8675fcdbb5a3ebe, Lean v4.30.0-rc2, and Mathlib
commit 5450b53e5ddc75d46418fabb605edbf36bd0beb6. The final declaration is
Domineering.berlekamp_conjecture_false in
Domineering/ReachableCounterexampleValue.lean.
The machine-readable ProofAtlas evidence record is
artifact.berlekamp-domineering-temperature-counterexample.reachable.v001.
It is also included in the public packet as
formalization/CHECKED_ARTIFACT.json.
Lean checks:
- the complete 30-move alternating replay from the rectangle;
- the board's exact equivalence to
{17/8 | -2+*}; - all 995,069 states of the complete difference-game certificate through a proved checker and ordinary kernel reduction;
- the explicit target's thermograph, temperature
33/16, and mean1/16; and - the resulting rectangle-reachable existential statement.
The development contains no sorry, custom mathematical axiom, or
native-decision shortcut. Python output and file hashes are not theorem
evidence.
The exact theorem uses the deliberately narrow predicate
HasValueTemperature: it exhibits a thermographed representative
game-equivalent to the board. The development proves that equality and the
representative's thermograph, but does not yet include a general theorem that
thermographs are invariant under every game-equivalence presentation. It also
does not formalize the one-cell deletion audit or separately formalize the
checkerboard obstruction for raw B.
Download and reproduce
The August 14 public artifact bundle
contains the matching paper PDF and LaTeX source, the complete Lean source and
generated certificate modules, Python verifiers and saved outputs, exact
evidence tables, the final SVG and PNG infographic, toolchain pins, and a
whole-bundle MANIFEST.sha256.
From the bundle root:
sha256sum -c MANIFEST.sha256
./RUN_ALL.sh
cd external_audit_2026-08-12
python3 independent_cgt_audit.py
python3 minimax_cross_check.py
python3 rectangle_reachability.py
To check the final Lean module from source, use the pinned toolchain and run
lake env lean Domineering/ReachableCounterexampleValue.lean inside
formalization/. The full generated certificate is included, but compilation
is a substantial resource job; build products are deliberately omitted.
Additional exact evidence
The non-Lean routes separately rederive the canonical game and thermograph, check the raw-option inequalities and their unique equality cases, replay the rectangle sequence, and prove the value equality again using ordinary win/loss minimax on a 1,039,152-state difference game.
For every one-cell deletion from the 26-cell core, the exact computed
temperature is below 2; the maximum is 15/8, attained at two cells. This
is deletion-local evidence only. It does not prove global size minimality,
uniqueness, or any minimality statement for the 28-cell reachable witness.
Review and priority boundary
The supplied evidence reports successful replays of the bundled Python routes. The checked-artifact record retains the successful cached Lean build transcript from the clean frozen source host, together with the no-sorry result, axiom profile, source commit, toolchain pin, and dependency-lock digest. ProofAtlas has matched the selected public files to the supplied manifest, but has not rerun the substantial Lean build for this page update. These checks were coordinated in the same author-directed workflow; they are not unrelated external replication or independent specialist peer review.
ProofAtlas does not award historical priority here. The manuscript reports
that the literature checked through August 12, 2026 contains no earlier
published Domineering position above temperature 2. A dedicated prior-art
review and a reproduction in an unrelated system remain worthwhile. It also
remains open how high finite Domineering temperatures can be and whether
there is an infinite family above 2.
Publication here records the exact supplied paper, visual, public bundle, and scoped Lean evidence. It does not substitute for unrelated reproduction, specialist peer review, or an independent historical-priority assessment.