A search that runs for thousands of candidates produces two things: a pile of failures, and — if it is logged properly — an argument about why they failed. These six plates are alternative readings of the same log. Each is built from the same three files, so whichever one you pick, the pipeline behind it does not change. Hover anything.
The headline is a flat line. 742 candidates were logged and 717 verified; 699 died on planarity.
Not one raised the bound. The best χ on a graph that actually splits into two planar layers is still 9,
exactly where Sulanke left it in the 1970s with K6 + C5. What the search produced instead
is closures: whole families proved incapable of containing a witness, which is what the
ledger records.
Append-only text, no database. A graph DB buys you nothing here — the log is written once, read whole, and never joined across. Thousands of rows is a 700 KB file.
| 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 |
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 all of them unchanged.