Work · External benchmarks
Thirteen problems we do not grade ourselves
An engine measured against its own criteria always ends up right. So we took thirteen open or competitive problems whose scoring belongs to someone else: public tables, official verifiers, named referees. This page states what passed, what failed, and what we had to withdraw.
Why external benchmarks
The rest of this site rests on protocols we write, fingerprints we compute, gates we define. That is checkable, but it is self-measured.
An open problem from the literature does not negotiate. The Packomania table is maintained by Eckard Specht; empty OEIS cells are empty for everyone; a board’s verifier returns an exit code that takes no account of our intentions. It is the only regime where being wrong costs something.
Every challenge follows the same procedure: a literature review before a line of code is written, a sealed pre-registration of what is sought and what will count as success, then mechanical certification. A challenge cannot start without its literature review — the launcher refuses.
The thirteen
| No. | Subject | State |
|---|---|---|
| 001 | Egyptian fractions 5/n (Erdős–Straus) | covering theorems proved algebraically · 1 claim withdrawn |
| 002 | Schinzel exceptions 20/n | 72 exceptions, no novelty — engine validation |
| 003 | Pomerance–Weingartner extension | 30 certified lists · OEIS drafts ready |
| 004 | IBM Ponder This, September 2026 | 45 terms — equals the reference, not a record |
| 005 | Packomania — free-radius circles | 60 candidate records + 155 first entries |
| 006 | Kobon triangles | 8 first bounds for empty OEIS cells |
| 007 | Fast matrix multiplication | Strassen certified by the Lean kernel, no axioms |
| 008 | Squares in a square | tool declared unfit — no attempt made |
| 009 | Chromatic number of the plane | two de Grey lemmas and the Parts graph verified |
| 010 | Integer complexity of 2⁶¹−1 | 133 ones against a baseline of 150, official verifier |
| 011 | Rational unit distances | 119 lower bounds revalidated by the official scorer |
| 012 | ESA SpOC — Programmable Cubes | in progress |
| 013 | Asymptotics of Σr | in progress |
Packomania — 60 certified candidates
The problem: place N circles of free radii in a unit square, maximising the sum of radii. The reference table is public and has been maintained for years; its holders are named — Specht, Tariq, Cantrell, Castro, Sander.
As of 16 September 2026 the dossier holds 60 candidate records and 155 first entries — cells the table left empty. That is 215 files, exact audit against the table of the day, 0 problems, and 60 Lean certificates verified with no axioms at all.
The submission dossier is assembled to be replayed by a third party: verifiers adapted to run from the folder, the reference table of the day, logs, SHA-256 manifest. The limits are written into it plainly — no optimality proved, first entries improvable, thin margins on four cells.
The word candidate is literal: the table moves. On the morning of 16 September, cell N = 119 was taken from us by a third party; it was pulled from the dossier, then won back that evening. A cell published by Castro above our value forced us to withdraw our entry. A record on a living table is not an acquisition, it is a position.
Kobon — eight empty cells filled
How many triangles can k lines form in the plane? The problem is open; the OEIS keeps the table, with empty cells.
Eight of those cells received a first lower bound: k = 35, 36, 39, 40, 43, 44, 47, 48.
And a result of a different kind: the author of a published dataset — Maiorana’s fifteen optimal arrangements at k = 14 — had asked for independent confirmation. Our two counters, written separately, each find 54 triangles across the fifteen. Confirming someone else’s work earns no record; it is nonetheless what the literature had asked for.
Chromatic plane — verify before claiming
How many colours are needed to colour the plane so that points at distance 1 differ? The question has been open since 1950. In 2018 Aubrey de Grey showed at least 5 are needed; the smallest known graph establishing it now has 509 vertices, due to Jaan Parts.
We did not beat that record. We did something else:
- Both of de Grey’s key lemmas were independently re-verified, with mechanical certificates: the negation encoded into clauses, refuted by a solver, then the proof re-read by a third-party checker. The larger runs to 6.32 MB and 2.6 million resolution steps.
- The Parts graph was re-read exactly — and the control refused our assumptions twice before passing: the graph does not live in the field we supposed, and one of its coordinates holds a nested radical.
- All 509 of its vertices are necessary: 509 criticality witnesses validated without a solver, 0 defects. Direct consequence — beating 509 requires new vertices; no subgraph will do.
Our best distinct 5-chromatic graph has 515 vertices. That is six too many. We write it down because it is the result.
What is not a record, said plainly
- IBM Ponder This — 45 terms. This arithmetic progression equals the length displayed by the reference (B. Felgenhauer). It does not exceed it. An exhaustive search for 46 terms came back negative below 10¹³.
- 20/n exceptions — 72 found. They recover a numerical fact already published by Pomerance and Weingartner. No mathematical novelty: the engine is validated, the mathematics does not advance.
- Chromatic plane — 515 vertices. Ten vertices above the record, and better intermediate values are already published. This is not a record and does not approach one.
What we withdrew
Five statements were annulled after being written. They appear here because a register containing only successes is not a register.
| Statement | Why it fell |
|---|---|
| Kobon: “UNSAT ⇒ a(18) = 93” | hidden modelling assumption — the encoding covered only simple arrangements, while the optimum at k = 8 uses triple points |
| IBM: “wall at 41 terms” | coverage artefact — three steps tested out of roughly eighty, mistaken for an impossibility |
| Chromatic plane: “only one translation class is good” | sampling artefact — four classes of twenty-four observed; the full sweep gives fourteen |
| 5/n: a generalisation | over-generalised before verification — the founding lesson of the closed vocabulary |
| Packomania: predictive value of a targeting tool | partly circular validation, caught at audit |
The most instructive challenge is a failure
On “squares in a square”, calibration scored 0 out of 2: the tool failed to recover two known configurations. It was declared unfit and no attempt was made on the open case.
A false improvement had been fabricated during development, then discarded by the control. That is precisely what calibration exists to catch — and why it is not skipped.
Scope of the result
- No submission has been sent. Drafts addressed to Specht, to IBM, to Maiorana and to the boards are ready; sending them is an act that belongs to the principal, not to the engine.
- Packomania records are candidates: no optimality is proved, and the reference table shifts underfoot.
- Kobon bounds and unit-distance tables are lower bounds. They prove no optimality.
- On the chromatic plane, nothing is claimed as new: two published lemmas were re-verified, a published graph was re-read. The value lies in the verification chain, not in the result.
- The individual contribution of each engine component is not established — an ablation study is proposed, not done.
- No cognition is established. The apparatus is a pipeline that generates, refutes and verifies; it does not invent proofs of named statements.
Public sources used under their licences: Maiorana’s data (CC BY 4.0), proof-checking tools under MIT licence, Parts’ coordinates unaltered. A dataset with no explicit licence was excluded from all use, its published results remaining citable only.