How the search works
Checking a labelling is easy. Trusting a trillion of them, computed on machines we do not control, is the actual engineering problem.
Splitting up the work
There is no list of six trillion trees to hand out — storing one would be absurd. Instead each task regenerates its own share. We use gentreeg, part of Brendan McKay's nauty package, which enumerates every unlabelled tree on n vertices exactly once and supports splitting that enumeration into mod disjoint classes. A task is then described by three small numbers:
(N, mod, res) — order N, class res of mod
Your computer receives those numbers, regenerates its slice of the tree list, and labels it. The input file is a few bytes; the work is hours.
Labelling one tree
- A deterministic heuristic searches for a graceful labelling within a fixed step budget.
- If the heuristic gives up, an exact search takes over with its own budget. Unlike the heuristic it is complete: within its budget, if it reports nothing exists, nothing exists.
- If both are exhausted, the tree is recorded as an explicit unresolved case — never silently dropped, and never reported as a counterexample.
Checking it — twice, independently
Every labelling is verified inside the application before it counts, by two checkers written separately that share no validation code with each other or with the search. Either one failing aborts the task. A third checker, written in Python from the mathematical definition rather than from the C source, re-verifies samples on the server.
The reason for the duplication is narrow and worth stating: a single checker that shares a bug with the search would confirm its own mistakes. Independent implementations do not usually fail the same way.
Why identical answers are expected
The result of a task is a pure function of its inputs. Two honest computers running the same task must produce byte-identical output files, so validation is an exact comparison rather than a fuzzy one. Holding that property takes real discipline in the application:
- No floating point anywhere that touches output. Integers only.
- No external randomness. The search uses a fixed pseudo-random generator seeded from the tree's own encoding — never the clock, the process id, or a memory address.
- Budgets are step counts, never seconds. A wall-clock cutoff would let a fast machine and a slow machine take different branches and produce different files.
- Single-threaded. No dependence on thread scheduling.
- Restart equivalence. A task you suspend and resume must produce exactly the file it would have produced if left alone.
Each task also carries a manifest hash pinning the source versions, generator options, both checkers, the seeding rules and both budgets. Change any of them mid-milestone and the outputs change, so we do not.
Counting the trees, not just trusting the count
Two obligations have to be met separately, and meeting one does not imply the other:
- Coverage — every distinct tree appears in exactly one class. Checked by reviewing the partition logic, by set-equality and uniqueness tests at small n where the full list fits in memory, and by reconciling the total against an independently computed A000055.
- Labelling — every generated tree gets a verified witness, or is an explicit unresolved case that blocks the milestone.
Matching totals alone are necessary but not sufficient: a missing tree balanced by a duplicated one gives the right count and the wrong answer. That is why the count is the last check and not the only one.
If a tree ever resists
A tree that survives both in-application searches is queued for unbounded admin-side work with no mathematical cutoff. If that returns "no labelling exists", it is checked again by a completely different method — a SAT encoding written independently from the definition, with a machine-checkable proof of unsatisfiability. Two timeouts are not agreement; only two validated exhaustive searches agreeing count.
Only if both agree does the tree become a candidate counterexample. At that point the milestone stops, and there is no announcement, no homepage banner and no forum post until humans outside this project have reviewed it. A false alarm here would be far more damaging than a slow one.
What we keep
We retain samples, cryptographic commitments to the full witness streams, and every exceptional case — not all trillions of labellings, which is not storable. Be clear-eyed about what that buys: this is a reproducible computational verification resting on reviewed software, not an independently checkable archive of every witness, and not a formal proof.
