The finished work, in one list

Self-published and not peer-reviewed. Each note states what it certifies, what it assumes, and what it will not claim; most ship the program that produced their numbers, and several run the argument live in the page. One ranked sequence, most important first — not grouped by theme, and since 13 August 2026 this index carries finished work only — the open notebooks, including the directions that went nowhere, live in the catalogue, with their verdicts, linked from every group’s note.

Every row carries a date. A plain date is the one the page prints itself. A date marked † is not stated on that page — it is when the file was first published to the repository, shown here so no row is undated, and it is this index’s claim rather than the page’s. Dates are publication, not last edit: a sitewide change touched all 35 files on 2026-08-05, so a modification time would say “today” for every row and mean nothing.

Every live report, most important first

One sequence, not themes. A report is on this list only if it claims something in its own bytes and a battery inside the build names it; everything else ships unlisted and is reachable by its own URL. Ordering weighs whether the object is external — someone else’s theorem, paper, benchmark or model — over whether it is ours, and whether the result is certified rather than illustrated.

• Erdős #290 — for even d, disc(f_d) is a square exactly at d = 4k(k+1), and here is why
  A certified bracket for the constant c in van Doorn’s lower bound, seven times narrower than the published 0.82 < c < 0.85: three Galois densities the paper left open, pinned exactly, and two further exceptional degrees beyond the range it computed. The degree pattern behind them — disc(f_d) a perfect square exactly at d = 4k(k+1) — is proved, not merely observed; whether the group drops at each such degree stays a per-degree question, answered through d = 120.
  2026-08-03 · seven programs, no dependencies · exact rationals + outward-rounded intervals · downloadable pack
• Maxwell said five charges allow at most 16 equilibria. At ε = 1/6, the counterexample’s 24 are now certified.
  The refutation’s published evidence was floating-point computer algebra — no code artifact, no certificate, no concrete ε. Pinned at the paper’s own Figure 1 configuration: 24 pairwise-disjoint Krawczyk boxes, each proving existence, local uniqueness and nondegeneracy of a critical point. And 24 > 16 in exact integers.
  2026-08-04 · CONFIRMED at ε = 1/6 · one pinned instance; the asymptotic statement is not audited
• A convergent flow finds the equilibrium. A certificate encloses it.
  An independent reproduction of the AIMS Mathematics 2026 multi-population Wardrop paper. Three scenarios, three different outcomes: one solved exactly over rationals, one certified by a Krawczyk argument, and one refused, because that instance admits more than one equilibrium.
  2026-07-23† · reproduction · the refusal is a result, not a gap
• An independent audit of OpenAI’s ten-proofs
  The Lean repository behind “Ten Advances in Mathematics” — built at its pinned commit (8666 jobs, exit 0), all twelve claimed declarations kernel-checked to exactly three classical axioms, the repo’s own cross-kernel Comparator protocol executed twelve-for-twelve, every challenge statement read against the manuscript’s theorems, and the week-one revision diffed. At challenge level, no statement weakening found — the discrepancies run the other way: the machine sometimes proves more than the paper claims, and the audit surface under-reports its own tree. With the shipped-configuration observation credited upstream, and the week the human authors wrote back.
  2026-08-14 · audit · build · kernel · cross-kernel · statements · diff
• Six AI-claimed results, re-checked. Five hold; the sixth holds on every fragment a machine can check.
  The index for the six below, and what the exercise actually found: on every one, the only check on record was the original author’s own.
  2026-08-03 · index · six independent re-derivations · five CONFIRMED, one PARTIAL
• Erdős #1038: every printed decimal of the extremal constant is right — and the 30th digit is a rounding, not an expansion
  An independent reimplementation — two interval backends, automatic differentiation, Krawczyk for existence and uniqueness — confirms all 30 printed decimals with certified enclosures to 40+ decimals, and finds the headline value’s last digit is a half-up rounding presented with an expansion’s trailing ellipsis.
  2026-08-04 · CONFIRMED · computational fragment; the extremality proof is not audited
• Testing that a verifier accepts correct answers does not tell you it rejects wrong ones
  Every auto-scored benchmark rests on a verifier, and the verifier is almost never audited — because auditing it looks circular. It isn’t, if you separate the directions. Across 103 verifiers that rejected every mechanically-broken variant, three independent adversaries still got past 13 of them, and five of those were rated sound by the other two attackers.
  2026-08-08 newest · measured, no model ranked · rates conditional on a perfect mutation score · the adversary corpus is withheld
• Ten HumanEval items killed every mutant thrown at them — and still accepted a solution proven wrong
  A perfect mutation score is not evidence that a test suite is sound. 14.7% of HumanEval items accept a candidate an independent witness proves wrong, and mechanical mutation rates 75% of those items as fine — so mutation-based sensitivity overstates suite quality. The page is generated from the measurement, and every one of the 163 items is listed with its witness so the claim can be checked item by item.
  2026-08-08 · measured, no model ranked · one candidate per item, an adversary-specific rate · the wrong-solution corpus is withheld
• Korenblum’s constant survives a second arithmetic
  A second implementation sharing no code with the first reaches the same bound.
  2026-08-03 · CONFIRMED
• A congestion mean-field game, enclosed — the certificate mechanism runs live in the browser
  Existence, local uniqueness in the full weighted-ℓ¹ ball — even and odd Fourier blocks — and strict positivity of the density, in outward-rounded interval arithmetic.
  2026-07-23† · single-file Python verifier · standard library only · runs in seconds
• One equilibrium, or three? — instance-level global-uniqueness certificates for mean-field games
  A checker that takes a concrete finite-state mean-field game and earns one of three verdicts in exact rational arithmetic: CERTIFIED-UNIQUE with the condition’s slack as an exact margin, an honest REFUSED naming the failing hypothesis, or MULTIPLE over the three machine-verified solutions of a published two-state game. The kernels run live in the page with falsifier buttons; the theorem is Cecchin–Di Persio–Fraccarolo’s, the witnesses are Cecchin–Dai Pra–Fischer–Pelino’s, and the page says so. A second condition family joined the same day: the monotonicity constant Gomes–Saúde assume and never compute, certified on their own illustration. Claim status on its face: conjectured, conditional on cited preprints. Companion note deposited at Zenodo (DOI 10.5281/zenodo.21922978). The verdict grammar has a routing-game sibling under Operations research — the air-taxi corridor report, where the refusal side becomes the exhibit: an equilibrium face certified exactly, instead of a point.
  2026-08-13 · runs in the page · exact rationals end to end · falsifier buttons
• Alien science needs a disposition, not a sermon
  A disposition procedure for machine-produced mathematics that no human has checked: what to run, what to refuse, and what the refusal costs. Added to this index 2026-08-21 — it had been live and listed in no group at all.
  re-run rather than believed
• No metric, no potential — a machine-checked certificate that a flow is not a gradient
  An exact-rational Sturm count certifies a complex eigenvalue pair at an equilibrium, ruling out every Riemannian metric and every potential at once. Two exhibits: softmax attention at engineered equilibria (224 of 864 certified; the d = 2 slice all-real by a theorem the census forced) and the Brusselator (37 of 60, an exact twin agreeing on all 60). Preregistered; both falsifiers carry a mutation-verified red; claim status on its face: conjectured.
  2026-08-12† · runs in the page · exact rational Sturm · falsifier buttons
• Ran–Teng Conjecture 20: every machine-checkable fragment holds. The analytic core is not audited.
  Re-verified in an independent reimplementation on an exact-rational and certified-interval stack: 43 checks, 0 failures, 5/5 mutation controls rejected. The proof’s analytic core is prose, was not audited, and the verdict is PARTIAL for exactly that reason.
  2026-08-04 · PARTIAL · fragment CONFIRMED, analytic core not audited
• The identities under the Mathieu–Zhao classification hold exactly
  The identities check out exactly. The theorem above them is still unchecked, and the note says so rather than letting the confirmation stand in for it.
  2026-08-03 · CONFIRMED · scope stated explicitly
• A power system priced live, every claim carrying its certificate
  A living note on price formation in a hydro-dominated system: the model is solved live in the page, and each claim carries the check that would expose it if it were wrong.
  runs in the page · no precomputed numbers
• The rank-two Poisson counterexample holds
  Re-derived in arithmetic sharing no code with the author’s.
  2026-08-03 · CONFIRMED
• The corridor totals are pinned. The operator split is not.
  An illustrative air-taxi corridor instance from the published structure of the Rio de Janeiro urban-air-mobility ConOps, solved in exact rational arithmetic: one scenario mathematically certified unique with an exact margin of 1, and one where the point-uniqueness certificate is honestly REFUSED — corridor totals pinned exactly, the two-operator assignment exhibited as a verified one-dimensional face of equally valid equilibria. The published verifier recomputes every number and ends with two mutation controls. In aviation “certified” is the regulator’s word; everything certified here is mathematics, and the page says so on its face.
  2026-08-13 · exact rationals end to end · the refusal is the finding
• Certify the machine’s candidate — the AI proposes; the certificate disposes
  A decidable pipeline for machine-generated mathematics: a candidate goes in, a certificate or an explicit refusal comes out, with no language model anywhere in the checking path.
  2026-07-23† · census of eight blind runs · reported as a census, never as a rate
• A mean-field game equilibrium, enclosed in your browser
  The page does not solve the equations and show you the answer — it solves them, then proves the answer: a radii-polynomial contraction argument, every inequality evaluated in outward-rounded interval arithmetic, returning either an explicit ball that contains an exact solution or a refusal. Includes a certified multiplicity result where uniqueness theory is silent.
  2026-07-28† · runs in the page · interval arithmetic + radii polynomial · refusal is an outcome
• Softmax sharpens with temperature. Here is the certificate.
  A certificate on a frozen attention row of a small GPT, with the fixture and a one-file verifier published beside it.
  2026-08-01† · certificate trio + fixture · verify_ml_beta.py
• The coordination thesis does not hold on the ONS population
  A negative result, stated as one: the effect the thesis predicts is not present in the data it was proposed for.
  2026-07-29 · negative result · published because it is one
• The preregistered prediction was 14/14 flips. The run measured 9/14 — five stages of my own certified chain invisible to its verdict.
  Truncation and single-stage corruption, reconstructed from the chain-of-thought faithfulness literature and aimed at this shop’s own certificate chain, with every prediction committed before the harness existed. The headline prediction was falsified, the blind spots were measured — and the chain was hardened the same day, errata Case 5.
  2026-08-05 · measured · causal step-importance, never model-CoT faithfulness · no shared scale with the papers it reconstructs
• A certificate should ship with its falsifier
  A proposal to the computer-assisted-proof genre: publish, beside every certificate, the mutation that makes its checker go red — the patch, both exit codes, the hashes. The mechanism is credited where it came from (mutation testing 1978; a blind seeded protocol with a placebo, Sandia 2000; mutation analysis for Coq, 2019); the August 2026 audit that found 11 proof-affecting defects in a published certificate shows what its absence costs; and all seven lane verifiers on this site already end with firing mutation controls — the practice, checkable now.
  2026-08-14 · proposal · the falsifier discipline, stated for the genre
• When enough agents interact, is equilibrium a point or a geometry?
  Where the equilibrium set stops being a point and starts having shape, and what can be certified about it once it does.
  2026-07-30 · mean-field limits · equilibrium structure
• How this shop runs — directing AI agents under falsifiable verification
  The methods essay. An agent’s output is a claim, never a result: no check counts until it has been seen failing on a deliberately broken copy, every agent carries a failure vocabulary that is scored as success, and the checks themselves are probed for vacuous passes — greens that verified almost nothing. Every number in the essay is a dated record rather than a live readout; the incidents are real, and the one still open is on the errata.
  2026-08-13 · essay · the method behind every other row on this page
• MFG Lab — equilibria you can check
  The instrument the rest of this shop was cut from: continuum mean-field games on one finite-difference kernel — a monotone upwind HJB operator and a Fokker–Planck operator built as its exact discrete transpose — plus the Wardrop/HRF network solver, run live in the page. Eight tabs, four of them a bench that exists to make the kernel falsifiable rather than to make a claim about the world. Every battery it is held to ships beside it.
  2026-07-21† · instrument · the kernel is the subject; the tabs are probes of it
• Make the resource finite and the price gains a second component — the water value
  A bounded reservoir turns the Gomes–Saúde price into a sum: the instantaneous clearing term plus a water value that is a martingale between binding times. Certified on a scenario tree. It is on this list for the first time today, and that is the correction: it has been exported, routed, indexable and in the sitemap while linked from no page at all — discoverable only to a crawler, never to a reader. No gate could see it, because link reachability was outside every gate’s scope until this one.
  2026-08-06† · certified on a scenario tree · the solve itself is withheld; the mathematics is not