The Heesch number world record (6, Bašić 2020) machine-decided exactly, with independently verifiable certificates

README.md

The Heesch number world record is exactly 6 — machine-decided, certificate included

The record for the largest known finite Heesch number is 6, set by Bojan Bašić's figure (Mathematical Intelligencer, 2021: https://link.springer.com/article/10.1007/s00283-020-10034-w). The published theorem claims Heesch number ≥ 6; the exactness details were deferred to a follow-up article that appears never to have been published. No coordinates and no checkable certificate for the record configuration were ever released.

This gist is the complete, self-contained evidence package — to our knowledge the first of its kind for the record:

1. A machine-checkable certificate that Bašić's figure admits 6 complete, hole-free coronas — 195 copies, 55,575 cells (witness_record_figure_6coronas.txt);
2. an independent verifier (verify_witness.py, pure Python, stdlib only, zero solver code) that checks certificates against the mathematical definition of a corona patch;
3. certificates for six more shapes in the same family, including the 2nd and 3rd shapes ever exhibited at world-record depth 6;
4. renders drawn from the certificates themselves (render_witness.py, PIL) — the three PNGs here;
5. PATCHES.md — the upstream solver bugs that had to be fixed before any record-scale output could be trusted, including one that silently emits garbage witnesses exactly at record scale.

The other direction — that no 7th corona exists (so the Heesch number is exactly 6, not just ≥ 6) — comes from an UNSAT verdict of a SAT-based search at maxlevel 7 (holes allowed), run to completion on a 1 TB machine. That half is solver-trusted, not independently certified; a DRAT/proof-logging trail is the natural upgrade.

The record configuration, drawn from its certificate

Center (yellow): Bašić's figure — six hexagons, eleven triangles, one half-triangle, 285 kisrhombille cells. Around it: six complete, hole-free coronas, 195 copies, 55,575 cells. Every pixel of this image is derived from witness_record_figure_6coronas.txt, not from the solver's internal state.

Verify it yourself (60 seconds)

python3 verify_witness.py witness_record_figure_6coronas.txt

Exit code 0 and OVERALL: PASS means: all 195 placements are genuine congruent copies (rigid motions on the [4.6.12] kisrhombille lattice), pairwise disjoint, every corona level is grounded and complete, every interior copy is fully surrounded, and the whole patch is hole-free (flood fill). The checker never invokes or trusts the solver. It was mutation-tested against deliberately corrupted witnesses (bad transform matrix, overlapping congruent copy, deleted placement, off-lattice translation — all correctly rejected).

For the three witness_*_holes.txt / inconclusive-format files, state the claimed depth explicitly:

python3 verify_witness.py witness_h8l_6coronas.txt --expect-depth 6

Results table

shape	cells	Heesch number	certificate
h5 (5-hexagon strip variant)	237	exactly 5 (witness + UNSAT@6)	witness_h5_5coronas.txt
Bašić's record figure	285	exactly 6 (witness + UNSAT@7)	witness_record_figure_6coronas.txt
lcap_full (record + 1 triangle)	291	exactly 6 (witness + UNSAT@7, two independent builds)	witness_lcap_full_6coronas.txt
h7 (7-hexagon strip)	333	exactly 6 (witness + UNSAT@7)	witness_h7_6coronas.txt
h7l	339	exactly 6 (witness + UNSAT@7)	witness_h7l_6coronas.txt
h8	381	≥ 6 with holes (a–d PASS; hole bounded by outermost corona); exact value open	witness_h8_6coronas_holes.txt
h8l	387	≥ 6 hole-free (all five conditions PASS); exact value open	witness_h8l_6coronas.txt
h9	429	≥ 6 with holes (a–d PASS); exact value open	witness_h9_6coronas_holes.txt

Before this, the literature contained exactly one shape ever exhibited at depth 6 (Bašić's). The table also kills the natural conjecture that lengthening the strip climbs the Heesch ladder (5 hexagons → 5, 6 → 6, so 7 → 7?): every member of the family decided at level 7 sits at exactly 6. The plateau is real.

Second shape ever at record depth (lcap_full, exactly 6):

The strip law's one confirmed step (h5, exactly 5):

Method / provenance

• Shape: transcribed cell-by-cell (285 kisrhombille "drafter" cells) from Figure 1 of Bašić 2021 and render-matched against the paper. The paper never published coordinates.
• Solver: Craig Kaplan's open-source heesch-sat (https://github.com/isohedral/heesch-sat) + CryptoMiniSat 5.14, with the fixes in PATCHES.md. The critical one: an unfixed FIXME in heesch.h solve() misroutes UNSAT-exactly-at-maxlevel into the inconclusive path, which then dumps a stale solver model with out-of-bounds reads — tens of thousands of phantom placements, silently, exactly at record scale. Without that fix (and a -DLARGEMEM=ON CryptoMiniSat build), no level-7 output can be trusted.
• Hardware: level-7 instances need roughly 100–150 GB of RAM (the record figure's level-7 run was jetsam-killed on a 128 GB machine at a true footprint of ~147 GB; completed on a 1 TB box, ~1.5–2 h per shape).
• Renders: render_witness.py reads only the witness file. Redraw them yourself: python3 render_witness.py <witness> out.png.

Witness file format

Line 1: the shape (cell coordinates, D = drafter/kisrhombille grid). Line 2: ~ hc hh n = conclusive record (hole-free Heesch number, holes-allowed Heesch number, number of patches), or ! n = solver-inconclusive at its max level (the witness still proves the depth it exhibits — that is what --expect-depth checks). Then one line per placement: <corona level> <a,b,c,d,e,f>, the affine map (matrix + translation) placing that copy on the lattice. Level 0 is the kernel; levels 1..6 are the coronas.

PATCHES.md

heesch-sat patches required at record scale

Upstream: github.com/isohedral/heesch-sat @ master, cloned 2026-07-29. Solver: cryptominisat 5.14.7. Build on macOS arm64, clang.

Patches applied to heesch-sat/src:

1. Makefile: include/lib paths /usr/local + /opt/local -> /opt/homebrew.
2. Makefile: -std=c++17 -> -std=c++20 (tileio.h uses templated-lambda NTTPs).
3. isohedral.cpp: add #include <map> and #include <vector> (libc++ only forward-declares via transitive includes; "too few template arguments").
4. Manual link step for sat: needs isohedral.o, which the Makefile omits: clang++ -L/opt/homebrew/lib -rpath /opt/homebrew/lib -lcryptominisat5
   -o sat sat.o isohedral.o
5. tileio.h + gen.cpp: line buffers 1000 -> 262144 bytes (285-cell drafter records are ~1700 chars; stock buffer causes infinite atoi loop).
6. cloud.h + surrounds.cpp: bitgrid<128> -> bitgrid<512> (285-cell figure pair rasterization exceeds the +-64 box; "Coordinate out of range").
7. heesch.h iterateUntilSimplyConnected: hole-banning clause read tiles_[index][lev] unconditionally, undefined when a hole tile has no level-lev variable (holes bounded partly by inner-corona copies) -- CryptoMiniSat "Variable N inserted, but max var is M" crash. Now negates the variable that was actually true in the model per placed tile (equivalent when defined, correct always). 8b. Same function, second hazard: the walkback runs on PAST solvers, created before later levels grew next_var_, so tiles can carry variable ids the old solver has never heard of -- add_clause aborts and model reads are out-of-bounds. Guard every variable use with < solver.nVars() (a tile absent from the solver's universe can never be placed by it, so skipping is exact).
8. heesch.h solve(): the author's own FIXME above the inconclusive test is real and worse than "minor". The level loop exits with level_ == maxlevel in two distinct cases -- SAT at every level through maxlevel (genuinely inconclusive) or UNSAT exactly at maxlevel (conclusive, Hh = maxlevel-1) -- and the old if (level_ == maxlevel) conflated them. In the UNSAT-at-maxlevel case it dumped past_solvers.back() (the maxlevel-1 solver) while getSolution walked tile variables up to level maxlevel: model[v] reads past the end of the model vector (UB; zeroed heap reads as l_True), so EVERY tile not placed at an inner level was spuriously reported placed at maxlevel. Observed signature: ! records with tens of thousands of placements, sane inner-level histogram, all-true outermost ring (73,929 and 107,665 phantom placements on two shapes). Fix: track failed_at_max in the loop and route that case to the conclusive branch, which already handles it (hh = level_-1, hole-free walkback). This is the bug that silently corrupts exactly record-scale runs. 9b. heesch.h getSolution(): bounds-guard model reads (v.second < model.size()). tiles_ can carry variable ids newer than the solver being dumped (extendLevelWithTransforms in the hh path; past solvers in the walkback). A variable outside the solver's universe can never have been placed by it, so skipping is exact; the unguarded read is UB and the root enabler of the bug in 9.

Linux build for level-7-class instances (2026-07-29): Debian/Ubuntu's packaged libcryptominisat5-dev ASSERTS on level-7-class instances ("Please compile with -DLARGEMEM" in watched.h -- clause IDs overflow 30 bits). Build CryptoMiniSat from source: apt cmake git zlib1g-dev libgmp-dev pkg-config; cmake -B build -DLARGEMEM=ON -DENABLE_PYTHON_INTERFACE=OFF -DNOM4RI=ON; install to a local prefix. GCC 15 also needs #include <algorithm> prepended to isohedral.cpp and words.h (same class as patch 3). Then compile -std=c++20 -O3 against the prefix and link with rpath to it. Level-7 UNSAT runs on the shapes here: ~100-150 GB peak RAM, 1.5-2 h each on a large box.

render_h5_5coronas.png

render_lcap_full_6coronas.png

render_record_figure_6coronas.png

render_witness.py

verify_witness.py

witness_h5_5coronas.txt

witness_h7_6coronas.txt

witness_h7l_6coronas.txt

witness_h8_6coronas_holes.txt

witness_h8l_6coronas.txt

witness_h9_6coronas_holes.txt

witness_lcap_full_6coronas.txt

witness_record_figure_6coronas.txt