Compute programs 4 campaigns · 224 threads · snapshot 819.2 h old34 days old

What is being decided right now.

Snapshot is 819 hours old. Figures below were true when written and may have moved since. The fleet publishes on milestones, not continuously.

The gate order

Desk gate → Sealed → Running → Verdict → Certified

No core-hours are spent before the desk gate clears and the prediction is sealed. Targets get killed at the gate, before a core-hour is spent — that is the gate working, not the program failing; the ones that died that way are listed at the foot of this page.

A satisfiability threshold that turned out not to exist

VERDICT

Does one integer predict whether a search sub-problem has a solution? The law was fitted on 6,353 distinct sub-problems across three sizes and looked like a clean flip from always-solvable to never-solvable. A fourth size, 324 sub-problems never used in the fit, refuted it.

bounds: boundary predicted at a constant offset of +9 above the theoretical minimum, from offsets of 9, 10 and 9 at three code sizes. On the completed fourth size the boundary is at +2 — seven below the sealed band. progress: REFUTED, and the cell is now completely decided: all 324 sub-problems at the fourth size, 145 solvable and 179 not. Satisfiability is not monotone in the statistic — unsolvable cases appear both below and above a fully solvable band at offset 8, which no monotone law can produce. The last seven cases were closed by a different method entirely, with machine-checkable proofs. on: numeris, etacompute, edison, synapse, einstein

sealed before first cycle: 0ffaa7bd4f0f6fa4…

Publishable either way — The refutation is the result: it produced the first completely decided cell in the project, and a structure we cannot yet explain.

CORRECTION. An earlier version of this page reported the law as confirmed and described the dataset as 12,758 sub-problems. Both were wrong. The count was inflated roughly twofold because every sub-problem was solved by two different solvers and the solver RECORDS were counted rather than the sub-problems. The confirmation was recorded on an unfinished experiment — 313 of 324 cases, with the missing eleven being the hardest and ten of them inside the region the claim was about. PRIOR ART: the statistic is not new. It equals the variance in row and column occupancy, which Kautz, Ruan, Achlioptas, Gomes, Selman and Stickel measured in 'Balance and Filtering in Structured Satisfiable Problems' (IJCAI 2001), and their finding that balance increases solving time is the same effect we observed. We report it as a replication, not a discovery.

PA(19,8,6) — a Handbook open cell

RUNNING

Does a 19-row packing array with 8 columns over 6 symbols exist? Equivalently: 19 golfers in 8 rounds with no repeated pair.

bounds: 18 ≤ pa(8;6) ≤ 19 (upper bound proved Aug 2026) progress: 0 solver-tasks decided, 0 satisfiable so far on: numeris (i9-14900K, 30 workers, hardest-cube-first)

sealed before first cycle: d26cb1bb4aae0e57…

Publishable either way — a satisfying assignment is a 19-row witness anyone verifies in milliseconds; exhaustion closes the cell at 18 and would be the first machine-checkable proof certificate published for a packing-array bound.

Desk gate cleared by reading the Kirkman-packing-design literature — the same object under a different community's name.

pa(7;6) — hunting a 25-row witness

RUNNING

Can 25 rows of length 7 over 6 symbols pairwise agree in at most one position? The standing record of 24 was set by heuristic search.

bounds: 24 ≤ pa(7;6) ≤ 31 progress: 3661 solver-tasks, 0 satisfiable, 663 inconclusive within budget on: etacompute + edison + synapse (disjoint shards) · einstein (long-budget pass on the inconclusive residue)

sealed before first cycle: fc74e61b413b44e1…

Publishable either way — a witness raises a bound that has not moved in 18 months; an empty sweep is published as evidence that 24 appears extremal, per the sealed resolution criterion.

The inconclusive cubes are not scattered — they concentrate where row and column occupancies are most uniform, which is also where the extremal objects live.

Butson-restricted measurement structures in dimension 6

SEALED

Can a fourth maximally-complementary measurement basis in dimension 6 be built from roots of unity? Dimension 6 is the smallest where the answer is unknown.

bounds: 3 known, 7 permitted by dimension; conjectured stuck at 3 progress: engine built with exact cyclotomic arithmetic; calibration against a 2007 published census must pass before any new claim on: queued on numeris (calibration) and einstein (corpus scan)

Publishable either way — each excluded class is a standalone result tightening a well-known conjecture; the calibration itself is a check on our own pipeline.

Complete classification lists have existed since 2020 with no exclusion work run against them.

Killed at the gate, with reasons

Targets we abandoned before or during compute. Recorded so they are not re-proposed, and because a program that only publishes its survivors is not showing you its evidence.

A₆(5,4) = 31 (= pa(5;6)) — independently proved and posted eight days before our verification finished; the lower bound had also been known since 2001. Our sweep agreed with both. Root cause: we searched three vocabularies for the object and missed the fourth.
A₆(6,5) = 27 — a predicted deficit law — SEALED AND REFUTED. The true value is 31, outside the stated falsification band. The law is dead; the flattening it exposed became the next question.
w(2;3,20), Erdős #176 cells, pa(11;8) — killed at the desk gate — each already settled, two under names we had not searched.