A portal · the number seam · made here, and checked to the bone
Made, Not Retold
Most of this archive explains known things, and tries to explain them beautifully.
This page is the other slice: the part that made things. Integer sequences that were not
in the record until they were computed here. New terms in sequences no one had touched for years.
Theorems proved with nothing imported. And, kept beside each one, the honest ledger of exactly how
far it is checked.
A corpus that only ever retold would be a textbook, and a lovely one. What makes a
claim original is that the number, or the proof, did not exist to be looked up. But there is
a trap in original work that retelling never faces: you cannot check it against the book, because
you are the book now. So the only thing that makes an original result trustworthy is the working
shown next to it, and the willingness to say, out loud, where the working is thinner than the claim.
This portal collates everything the Wasteland made, sorted by exactly what kind of new each one is,
and it ends by turning that same knife on its own receipts.
new sequence, absent from OEISnew term in a published sequencemachine-checked, zero importestimate, exact value openwithdrawn, proved not new
§1 Recompute it yourself
Do not take the number on faith. Watch it get made.
Three of the sequences below are cheap enough to recompute from scratch in your
browser. Pick one and a size, and this panel runs the definition live, then checks the result
against the value committed to the repository. It is the same from-scratch code that this page's
offline verifier runs (research/made-not-retold/verify.mjs), which reproduces the small
terms of eight of these result families and matches the committed data on 328 / 328 checks.
§2 New sequences, absent from the record
Objects that were not in the encyclopedia until they were counted.
Each was computed by an exact method (enumeration, exact recursion, or exact-rational arithmetic,
never floating-point estimation), checked against a second value or method, and confirmed absent
from the Online Encyclopedia of Integer Sequences at the time of writing. The order below runs from
the results whose independent verification is strongest to the ones that honestly rest on a single
path at their largest terms. Where the coverage audit (see §6) narrowed a claim, that is written
into the line.
Not a new object, but a value nobody had computed.
These extend sequences the encyclopedia already lists but leaves marked more,
the flag that says the authors could not go further. Extending one is a smaller, sharper kind of
original: every published term is reproduced first, and then the ground continues past where it stopped.
Proofs a kernel accepts, built from the bare language.
These do not claim new theorems. What is original is the proof artifact: each is written in Lean 4
with an empty import list, no mathlib, no standard library, so the only thing
trusted is the bare proof kernel. Across all eighteen source files there is no realsorry and nonative_decide: every one is checked by
the kernel itself, not by compiled code. That makes this the most solid corner of the whole archive, and the
lines below say honestly which are proved for every case and which are verified for specific ones.
The estimate that never became a term, and the claim the rule caught.
The never-lie rule is only worth anything if it costs you something, so here is where it did. One
headline result is an estimate the project refuses to write as an exact term. Two others were staged
as discoveries and then withdrawn when the project proved they were already known.
A page collating original work owes you one more thing: not just the results, and not just their
checks, but an honest account of how good the checks are. The project ran that account on itself.
The coverage audit, 20 July 2026
It began with an embarrassment. A graceful-labeling pair had landed as "confirmed two ways" when
both ways were one engine run twice. So twenty read-only agents audited every staged sequence
directory the same way, comparing each directory's words about its verification to what its
committed code actually evaluates. All twenty-one directories overclaimed at their largest
terms. The recurring faults: a verifier whose hardcoded range stops short of the staged b-file,
so it prints ALL PASSED without ever touching the newest value; "N independent methods" that overlap
only on the small cases, leaving the top term on a single path; one path re-run with different flags
and counted as two; and, in one case, a confirming run the computing session reported but never
committed, so the claim is unreproducible.
The distinction that matters here: the terms are not suspected wrong.
No value has been contradicted. It was the sentences about the verification that were stronger
than the verification. Under a rule whose whole content is do not overstate what you have shown, that
is precisely the failure that counts, which is why it is on this page and not hidden. A correction
wave the same night rewrote five directories to state per-term coverage (which term rests on which
path) and extended verifiers where a cheap run closed the gap; it was cut off by a usage limit with
sixteen still open. Those sixteen are marked in their own directories and, where it changed a
claim, on the lines above.
The check, and its edges
Nothing here is asserted from memory; the numbers on this page are read from the committed b-files,
and a verifier written fresh for this portal recomputes the small terms of eight of these families
from scratch, sharing no code with the engines that produced them. It matches the committed data on
328 / 328 checks: topswops, the Lucas-Lehmer graph, Gardens of Eden, the streak
rationals, Bulgarian settling, graceful totals, and the leapers on both surfaces, the last also
pinned against the published flat-board counts as external ground truth.
Source: research/made-not-retold/verify.mjs.
What the recompute covers: the low range, exactly, by an independent implementation. A live match at small n is a real second witness, and it is the witness the audit found the corpus was often missing.
What it does not cover: the largest terms of most sequences, which are past what a from-scratch check can cheaply reach. Those rest on each result's own verifier, whose true per-term coverage is now stated in its directory, sixteen of them still carrying the caveat that the top term rests on one path.
The machine-checked results stand apart: zero imports, no sorry, no native_decide, kernel-checked. Their edges are scope, not trust, and each is labelled above (all-n, necessity-only, or specific instances).