Every graph below has been verified biplanar: its edges really do split into two planar layers, and the colouring shown is one a solver actually found. Map draws each layer as a world whose countries border each other exactly when that layer holds their edge, so adjacency is something you can see. Graph draws the same two layers as straight-line planar embeddings, which is the view that lets you check the claim rather than take it.
The lower bound has not moved. No graph here needs ten colours; χ = 10 is empty and the
filter says so. What the search has built instead is a set of walls around where a ten map could
live. Every biplanar graph on at most 17 vertices is 9-colourable, extending
Kirchweger–Scheucher–Szeider's n ≤ 13 (SAT 2023) by four vertices
(f100). Ten vertices are fully classified: a graph on ten vertices
is biplanar exactly when its complement contains two disjoint edges (f487).
And the independence route is pinned: no biplanar graph on 19 or more vertices has
independence number at most 2 (f494, f032), and one with independence
number at most 3 has at most 30 vertices (f495), so a ten map of that kind has exactly
28, 29 or 30.
On novelty, carefully. Sulanke's K6 + C5 is the famous 9-chromatic biplanar
graph, but it was never the only one: Boutin, Gethner and Sulanke published forty more on
12–16 vertices in 2008, plus a proven infinite family. Five graphs this project first called new
turned out to be exact rediscoveries of theirs, proved by explicit isomorphism
(f123, f124). Of the corpus below, seven 9-critical graphs match
nothing in the published record (f126). The rest are verified, and
worth looking at, without being new.
Give every country a twin that borders it and has exactly the same neighbours. A 28-vertex graph in which every vertex has such a twin is the doubling of a 14-vertex graph Q, and doubling keeps the largest set of mutually non-adjacent vertices the same size. If that size is at most 3, the 28 vertices need at least ten colours, so a single doubling that splits into two planar layers would be a ten map, with the layers as its proof. Necessary conditions leave finitely many shapes for Q, and the search is deciding every one of them.
| edges in Q | classes | ruled out by f025 | by solver | by heredity | open |
|---|
Append-only text, no database. A graph DB buys you nothing here: the log is written once, read whole, and never joined across, and the whole of it loads in one fetch.
| path | shape | what it is for |
|---|---|---|
| data/attempts.jsonl | one JSON object per line | every candidate tested, ~450 bytes each, no edge lists |
| data/detail/<id>.json | one file per flagged row | full edge lists, layouts, colouring witness — only for rows worth drawing |
| data/ledger/findings.jsonl | append-only, superseding | durable structural claims + the attempt ids that earned them |
| data/ledger/queue.json | hand-editable array | next actions, carried between sessions |
| data/ledger/LEDGER.md | generated | the human-readable render; never hand-edited |
| data/index.json | manifest | counts, families, featured ids — what this page reads first |
| data/clone_status.json | generated | the cloned-countries tally above, rebuilt from the search's own records at every deploy |
The split matters: keeping edge lists out of the main log is what lets the whole search stay greppable
and load in one fetch. rlog.py writes all of it — brief before a session,
attempt per candidate, finding per conclusion, render at the end.
A search that does not remember itself pays for every dead end twice. rlog.py is the
memory: one command at the start of a session, one per candidate, one per conclusion.
| command | when | what it enforces |
|---|---|---|
| rlog.py brief | first thing, every session | bounds, closed families and why, working techniques, open questions, nearest misses, next actions |
| rlog.py check --family X | before committing to a family | blocks a family the ledger closed; you may proceed only by naming the new idea that breaks the stated reason |
| rlog.py attempt --file r.json | per candidate tested | required fields, bounds sanity checks, edge lists split into the sidecar |
| rlog.py finding --kind … | per durable conclusion | a ruled_out claim without evidence ids is refused outright |
| rlog.py render | end of session | rebuilds LEDGER.md and index.json from the logs |
Findings are append-only. A claim is never deleted, only retired by a later one that names it in
supersedes — so the ledger keeps the argument, not just the current answer. Read it
at ledger.html.
If you are a language model asked to work on this problem, read FOR_LLMS.md first. It is written to get you to the research frontier in one pass, so you do not spend context rediscovering settled ground.
| read | for |
|---|---|
| FOR_LLMS.md | the whole state of the art: bounds, closed families, open fronts, verification standard |
| HIGHLIGHTS.md | the short version — what is proved versus evidenced, and which results may be new |
| the ledger | every claim with its evidence ids, by category |
| PROMPT.md | the operating brief, including the protocol for claiming a result |
Two things will save you the most time. Check the corridor first —
ceil(9n/2) ≤ m ≤ 6n−12 kills a large fraction of proposals by arithmetic alone. And run
rlog.py check --family X before committing to a family; it blocks one the ledger has
already closed, and you may proceed only by naming the new idea that breaks the stated reason.
attempts.jsonl redraws it unchanged.