Generate at scale, screen in float, certify the survivors exactly. Every number below was read off a record when this page was built, and every battery it reports green was executed during that build.
Published, not peer-reviewed, not independently rerun. Every claim below is rerunnable from the public repository; external reruns will be recorded here as they arrive — none has yet. Enclosures are proofs-of-object pending that independent verification.
| family | what a hit asserts | generated | screened | certified → hit | stop |
|---|---|---|---|---|---|
| chowla-cosine | a finite integer set whose certified Chowla merit c = -min f_A / sqrt|A| falls below 1 | 400,000 | 1,579 | 1579 → 1508 | exhausted |
| erdos852-constants | a constant holding up the conjectured asymptotic h(x) ~ c0 log x on Erdős #852, replaced by a certified interval enclosure — and its published decimal decided exactly against that enclosure | 4 | 4 | 4 → 3 | exhausted |
| henon-census | a parameter pair (a,b) and period p for which the number of period-p points of the Hénon map is determined EXACTLY: every fixed point of H^p enclosed in a certified uniqueness box, the rest of the plane excluded by interval arithmetic | 328 | 328 | 328 → 328 | exhausted |
| henon-orbits | a parameter pair (a,b) and an explicit box in which the Hénon map provably has a periodic orbit of period p, and exactly one | 3,936 | 1,023 | 228 → 228 | exhausted |
| holmes-census | a parameter pair (d,b) and period p for which the number of period-p points of the Holmes cubic Hénon map is determined EXACTLY: every fixed point of H^p enclosed in a certified uniqueness box, the rest of the plane excluded by interval arithmetic | 124 | 124 | 124 → 124 | exhausted |
| keller-audit | an explicit polynomial map C^n -> C^n whose Jacobian determinant is proved constant by symbolic expansion over exact rationals, with certified distinct rational points sharing one image — the Jacobian conjecture refuted in dimension n, decided here and not trusted | 11 | 11 | 11 → 11 | exhausted |
| keller-fibers | a Keller map and a rational target with AT LEAST k certified preimages — pairwise-disjoint Krawczyk boxes found by blind multistart Newton on the exact map; k >= 2 re-proves non-injectivity with no witnesses consumed | 9 | 9 | 9 → 7 | exhausted |
| newman-minmod | an n-term Newman polynomial whose certified min|f| on |z|=1 exceeds every value achievable with fewer terms | 400,000 | 7 | 4 → 4 | exhausted |
| oeis-closedform | a published OEIS constant whose record — name AND fetched formula/comment fields — states no closed form, while its digits are consistent with a small closed form and every other form in the vocabulary is refuted | 14,677 | 14,593 | 14593 → 0 | exhausted |
| ramanujan-audit | a published Ramanujan Machine conjecture re-evaluated as a rigorous enclosure and decided against the claimed closed form — survival certified to the enclosure width, refutation proved (and, for their corpus, a discovery) | 52 | 52 | 52 → 51 | exhausted |
| strassen-audit | a claimed fast matrix-multiplication algorithm — a rank-r decomposition of the (n,m,p) tensor — whose defining identity (nm·mp·np exact equations) is VERIFIED over the claimed ring with r strictly below the naive nmp; the C-layout convention is detected and recorded, never assumed | 11 | 11 | 11 → 10 | exhausted |
The screen is float and may only ever prune; nothing is admitted without an exact certificate. A family plugs in by supplying six functions — enumerate, value, interesting, certify, key, statement — and inherits the loop, the scale and the dedup.
| family | object | certified enclosure | width | closed forms refuted |
|---|---|---|---|---|
| chowla-cosine | [1,2,4,6,7,8] | [0.649862827152, 0.649862827152] | 5.55e-16 | 715 / 715 |
| chowla-cosine | [1,2,3,5,6,7,8] | [0.715658879606, 0.715658879606] | 5.55e-16 | 716 / 716 |
| chowla-cosine | [1,2,3,5,7,8,9,10] | [0.715967581851, 0.715967581851] | 5.55e-16 | 716 / 716 |
| chowla-cosine | [1,2,4,6,8,9,10] | [0.725127302045, 0.725127302045] | 5.55e-16 | 718 / 718 |
| chowla-cosine | [1,2,3,5,6,8,9,10,11] | [0.725987311197, 0.725987311197] | 5.55e-16 | 718 / 718 |
| chowla-cosine | [1,3,4,5,6,9,10] | [0.742177616900, 0.742177616900] | 5.55e-16 | 718 / 718 |
| chowla-cosine | [1,4,5,6,9,10] | [0.742222719215, 0.742222719215] | 5.55e-16 | 718 / 718 |
| chowla-cosine | [1,2,4,5,6,9,10,11] | [0.750810171748, 0.750810171748] | 6.66e-16 | 718 / 718 |
| chowla-cosine | [1,2,3,4,6,8,9,10,11,12] | [0.759444373892, 0.759444373892] | 5.55e-16 | 717 / 717 |
| chowla-cosine | [1,2,3,5,8,10,11,12,13] | [0.759942805134, 0.759942805134] | 6.66e-16 | 717 / 717 |
| chowla-cosine | [1,2,3,4,8,10,11,12,13,14] | [0.763617416452, 0.763617416452] | 5.55e-16 | 717 / 717 |
| chowla-cosine | [1,3,4,7,8,10,11] | [0.763698607335, 0.763698607335] | 8.88e-16 | 717 / 717 |
| erdos852-constants | [erdos852-c0-enclosure] | [1.323228276864, 1.323228276864] | 2.22e-16 | 719 / 719 |
| erdos852-constants | [erdos852-c0-digits] | [1.323228276864, 1.323228276864] | 2.22e-16 | 719 / 719 |
| erdos852-constants | [erdos852-cstar-enclosure] | [0.075240386178, 0.075240386178] | 3.33e-16 | 703 / 703 |
| henon-census | [1.4|0.3|8] | [64.000000000000, 64.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.34|0.3|8] | [48.000000000000, 48.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.36|0.3|8] | [48.000000000000, 48.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.38|0.3|8] | [48.000000000000, 48.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.14|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.16|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.18|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.2|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.22|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.24|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.26|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-census | [1.28|0.3|8] | [32.000000000000, 32.000000000000] | 0.00e+0 | 0 / 0 |
| henon-orbits | [0.6|0.3|1|0.833333333] | [0.833333333333, 0.833333333333] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.62|0.3|1|0.825297414] | [0.825297414485, 0.825297414485] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.64|0.3|1|0.817519468] | [0.817519468482, 0.817519468482] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.66|0.3|1|0.809985304] | [0.809985304012, 0.809985304012] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.68|0.3|1|0.802681828] | [0.802681828468, 0.802681828468] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.7|0.3|1|0.795596939] | [0.795596939087, 0.795596939087] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.72|0.3|1|0.788719427] | [0.788719427131, 0.788719427131] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.74|0.3|1|0.782038893] | [0.782038893311, 0.782038893311] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.76|0.3|1|0.775545673] | [0.775545672898, 0.775545672899] | 2.02e-13 | 0 / 0 |
| henon-orbits | [0.78|0.3|1|0.769230769] | [0.769230769231, 0.769230769231] | 2.01e-13 | 0 / 0 |
| henon-orbits | [0.8|0.3|1|0.763085795] | [0.763085794519, 0.763085794519] | 2.02e-13 | 0 / 0 |
| henon-orbits | [0.82|0.3|1|0.757102917] | [0.757102917009, 0.757102917009] | 2.01e-13 | 0 / 0 |
| holmes-census | [2.7|0.2|4] | [49.000000000000, 49.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.775|0.2|4] | [49.000000000000, 49.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.85|0.2|4] | [49.000000000000, 49.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.55|0.2|4] | [33.000000000000, 33.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.625|0.2|4] | [33.000000000000, 33.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [1.95|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.025|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.1|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.175|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.25|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.325|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| holmes-census | [2.4|0.2|4] | [17.000000000000, 17.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Meng–Yang arXiv:2607.22198|5] | [128.000000000000, 128.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Gallagher zenodo.21479195 d=2|3] | [1.000000000000, 1.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Gallagher zenodo.21479195 d=3|3] | [1.000000000000, 1.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Gallagher zenodo.21479195 d=4|3] | [1.000000000000, 1.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Gallagher zenodo.21479195 d=5|3] | [1.000000000000, 1.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Gallagher zenodo.21479195 distinct member (w-2w^3)|3] | [-1.000000000000, -1.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Alpöge 2026-07-19|3] | [-2.000000000000, -2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [Alpöge 2026-07-19|8] | [-2.000000000000, -2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [tangent-sweep d=3 (new curve through the published mechanism)|3] | [-2.000000000000, -2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [tangent-sweep d=4 (new curve through the published mechanism)|3] | [-2.000000000000, -2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-audit | [tangent-sweep d=5 (new curve through the published mechanism)|3] | [-2.000000000000, -2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|alpoge] | [3.000000000000, 3.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|alpoge-own-target] | [3.000000000000, 3.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|sweep-d3] | [3.000000000000, 3.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|gallagher-d2] | [3.000000000000, 3.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|gallagher-d3] | [3.000000000000, 3.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|sweep-d4] | [2.000000000000, 2.000000000000] | 0.00e+0 | 0 / 0 |
| keller-fibers | [fiber|gallagher-distinct] | [2.000000000000, 2.000000000000] | 0.00e+0 | 0 / 0 |
| newman-minmod | [0,2,4,5,8,9,10,11,12] | [1.362373178133, 1.362373178133] | 4.44e-16 | 720 / 720 |
| newman-minmod | [0,6,8,12,13,15,16,17] | [1.254933139031, 1.254933139031] | 6.66e-16 | 719 / 719 |
| newman-minmod | [0,3,8,12,13,14] | [1.013007454017, 1.013007454017] | 6.66e-16 | 694 / 694 |
| newman-minmod | [0,2,7,8,11,12] | [1.009230830699, 1.009230830699] | 4.44e-16 | 689 / 689 |
| ramanujan-audit | [rm-cat-22] | [21.310733573145, 21.310733573145] | 7.11e-15 | 719 / 719 |
| ramanujan-audit | [rm-z2-new8] | [18.190787907439, 18.190787907439] | 1.07e-14 | 719 / 719 |
| ramanujan-audit | [rm-cat-21] | [17.310693507032, 17.310693507032] | 7.11e-15 | 720 / 720 |
| ramanujan-audit | [rm-cat-18] | [13.966059953644, 13.966059953644] | 3.55e-15 | 715 / 715 |
| ramanujan-audit | [rm-z2-new7] | [13.382476033966, 13.382476033966] | 3.55e-15 | 719 / 719 |
| ramanujan-audit | [rm-zo-z5z3c] | [12.993891508980, 12.993891508980] | 3.55e-15 | 704 / 704 |
| ramanujan-audit | [rm-cat-19] | [12.735713658946, 12.735713658946] | 5.33e-15 | 719 / 719 |
| ramanujan-audit | [rm-z2-new4] | [12.382476033966, 12.382476033966] | 7.11e-15 | 720 / 720 |
| ramanujan-audit | [rm-cat-17] | [11.704592362598, 11.704592362598] | 5.33e-15 | 705 / 705 |
| ramanujan-audit | [rm-cat-20] | [11.126365014738, 11.126365014738] | 7.11e-15 | 720 / 720 |
| ramanujan-audit | [rm-z2-new9] | [9.627705192345, 9.627705192345] | 3.55e-15 | 719 / 719 |
| ramanujan-audit | [rm-z2-new5] | [8.557960170974, 8.557960170974] | 7.11e-15 | 720 / 720 |
| strassen-audit | [mm|alphatensor-f2-5x5x5] | [96.000000000000, 96.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-q-4x5x5] | [76.000000000000, 76.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|strassen-squared-4x4x4] | [49.000000000000, 49.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-q-4x4x4] | [49.000000000000, 49.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphaevolve-48-4x4x4] | [48.000000000000, 48.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-q-3x4x5] | [47.000000000000, 47.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-f2-4x4x4] | [47.000000000000, 47.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-q-3x3x3] | [23.000000000000, 23.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|strassen-1969] | [7.000000000000, 7.000000000000] | 0.00e+0 | 0 / 0 |
| strassen-audit | [mm|alphatensor-q-2x2x2] | [7.000000000000, 7.000000000000] | 0.00e+0 | 0 / 0 |
Each row is an exact enclosure, not a measurement. The last column is the engine asking whether the value has a small closed form: every candidate lying outside the enclosure is refuted exactly. The Ramanujan Machine matches truncated decimals and argues from collision probability; this decides.
54,629,173 candidate closed forms were tested against certified enclosures around 1e−15 wide, and 54,628,275 were refuted exactly — the value provably lies outside. Zero survivors means these objects have no small closed form of the shapes searched: a proved negative, not a failed search.
The count decomposes with nothing folded in: 54,629,173 tested = 54,628,275 refuted in double + 21 refuted exactly in BigInt + 877 with the form already on the OEIS record + 0 open + 0 surviving. Forms the 17-digit double screen could not separate were re-decided at the full published digit length in BigInt; forms OEIS already states are the record check working, not discoveries; the subtraction closes to zero and the engine refuses to write a ledger where it does not.
| bar | certified min|f| to beat | source |
|---|---|---|
| bar(6) | 1.000000000000000 | literature / lab |
| bar(7) | 1.065285891134415 | literature / lab |
| bar(8) | 1.101882938486186 | literature / lab |
| bar(9) | 1.311101302872326 | literature / lab |
| bar(10) | 1.378187726393090 | adopted here |
| bar(17) | 1.899892237678303 | adopted here |
| bar(18) | 1.899892237678303 | adopted here |
| bar(19) | 1.899892237678303 | adopted here |
| bar(20) | 2.018174563075912 | literature / lab |
Anchors from the literature and the source lab, plus objects this lab certified and then adopted. Both stored as witness sets and re-certified at load, so no value is transcribed. Frozen at load — the bar never moves under a running campaign, or a candidate's verdict would depend on when it was proposed.
The bars at n = 10 and n = 17 MOVED in August 2026 — bar(10) to 1.3782 past Boyd's 1986 witness, bar(17) to 1.8999 via the certified n = 13 box champion — because the exhaustive box30 sweeps behind certs/mu-table.json certified minima exceeding what the literature and the source lab held. A returning reader's remembered bar is stale because the mathematics improved, not because anything drifted; the rows tagged "adopted here" are exactly those promotions.
Staleness audit: clean — nothing certified sits above the envelope unadopted.
| battery | covers | this build |
|---|---|---|
| funnel machine | 14 items · 19 red controls | green |
| detach | 11 checks | green |
| interval · eqcert | falsifier-required certificates | green |
| interval · arithmetic | 16 000 ops vs exact rationals | green |
| interval · transcendental | sound exp/log/sin/cos | green |
| trigmin certifier | 47 checks · 2 red controls | green |
| newman box sweep | Goddard's 1992 box re-closed every run, cross-lab counts pinned; 100% kill audit · 7 red controls | green |
| lambda sweep | Mercer's proved closed forms computed, never remembered; the wrong-endpoint bar refused by name and shown fatal · 4 red controls | green |
| mercer mu5 ladder | mu(5) <= 1 + pi/m certified m = 5..20; Mercer's Tables 5-7 reproduced, the source-lab m=6 record matched, every case point re-proved · 5 red controls | green |
| census (henon + holmes) | closed-form calibration, two maps · 5 red controls | green |
| keller audit + sweep | symbolic det over Q, generator calibrated on Alpöge · 4 red controls | green |
| cf audit | all seven Ramanujan Machine sheets — 51 printed rows + the certified correction (e, pi, zeta(3), Catalan, pi^2, ln 2, mixed zeta orders) · 10 red controls | green |
| entropy covering | certified h_top lower bounds; ln 2 calibration at the full horseshoe · 4 red controls | green |
| strassen audit | fast-matmul tensor identities over Q and F2; Strassen 1969 calibrates · 3 red controls | green |
| bigfloat layer | directed-rounding big-float intervals; pi/ln2/e to 50 literature digits · 5 red controls | green |
| erdos852 constants | certified c0 and C* enclosures; pi^2/8 product calibration · 5 red controls | green |
| engine + families | red controls on screen and certifier | green |
| keller · standalone re-verifier | the detached certificate re-audited from scratch — stdlib fractions, no code from this repo; red control must fire | green |
| strassen · standalone re-verifier | every matmul identity re-derived in stdlib Python ints; pins re-hashed; red control must fire | green |
| erdos852 · standalone re-verifier | the C* refutation re-proved in exact stdlib ints (no tail, no rounding); the c0 window re-decided at 130 digits; 4 red controls must fire | green |
| sos · global bound | stdlib fractions only | green |
| sos · lyapunov | stdlib fractions only | green |
| sos · re-verify AI result | stdlib fractions only | green |
| llm harness — the eval's dry-run gate | a FAKE proposer gates the pipeline, not an LLM result; live model campaigns are separate, in the append-only certs/matmul-eval-ledger.jsonl and on reports/matmul-eval.html · aborts if a red control certifies | green |
Lifted from the source lab: 99 files, 4 patched on the way in, each patch declared. Drift now: 99 unchanged · 0 source moved · 0 local edited · 0 source gone. The source lab (sin-mfg) is read-only, permanently — read anything, never write, and report an error there rather than repair it.