A research programme is only as good as the things it has already closed. This page is the board: what is done and checkable today, what survived deliberate attempts to break it, what was refuted and published anyway, what the literature pass killed before prose, and what is being worked on now.
The last two numbers are the ones that matter. A refuted claim is a result and is published like any other — a programme with no refutations has either been lucky or has not been looking. And the top rung is empty by construction: it requires a named human reviewer who has tried to break the work, which is the one thing one person cannot supply.
Each of these is open, and each ships the verifier that produced its numbers. The figures below are measurements, not claims about measurements — you can reproduce every one.
To our knowledge the first validated-numerics enclosure of a stationary mean-field game with congestion. Existence, local uniqueness within the even (cosine) subspace, and strictly positive density, all in outward-rounded interval arithmetic. The verifier is one file, standard library only, and finishes in about two seconds.
An independent, proof-carrying reproduction of a 2026 AIMS Mathematics paper on multi-population Wardrop equilibrium. Three scenarios, three honest outcomes: one refuses, one is solved exactly over rationals, one is enclosed by a Krawczyk argument. Errata found in our own work are published on the page beside the result.
Price formation under a stock constraint — the calculation behind hydro dispatch and storage bidding — certified by zero-gap linear-programming duality on a scenario tree. The sign of the gap is load-bearing: weak duality makes a negative value structurally impossible, so a negative gap would be a defect in the formulation, not a tolerance.
A proposed law held on 508 clean samples and was then killed by an explicit counterexample. It is recorded as refuted rather than quietly dropped, because a programme that only records its survivors is indistinguishable from one that never tested anything. The refutation is the result.
eqcert: one interval-arithmetic library, one exact-rational library, and the
contraction operators that turn a numerical candidate into a proof — radii-polynomial
and Krawczyk. A Certificate cannot exist without a falsifier, enforced in the type
rather than remembered: a PROVED verdict carrying no evidence throws.
Honest faces at the stage they are. Each carries a draft banner and page-state badges. This list is the short route into the live draft pages; Program is the index.
Candidates are triaged before they are started, and most do not survive triage. Of nine proposed, four were cut: two were already certified here, one had been refuted by counterexample, and one turned out to be standard monotonicity theory wearing a new name. The triage is itself an output — the pattern it exposed is that every survivor has a parameter in it, and is certifiable by bracketing rather than by solving.
Not one equilibrium but a map of where behaviour changes across a parameter box: where the density concentrates, where uniqueness is lost, where the proof must refuse. Two earlier candidates contradicted each other until the honest object turned out to be a sign condition on the coupling rather than a threshold in a parameter — which is why the combined question survives and neither half does alone.
Bracketing the extremum of a price under a stock constraint, rather than solving for it. The same shape as the water-value result already closed, extended from a point to a range — the direct commercial continuation of the energy work.
Certificates are stronger when two independent implementations agree. The congestion result already has this — a Python verifier and a JavaScript one agreeing to the last bit. The work is extending that property to the rest of the board, so no certificate rests on a single implementation of the arithmetic.
What would change these rows. A counterexample to any claim on this page is the most valuable thing anyone could send, and it would be published like any other result — with the sender's name on it if they want it there. Send one →
And what will not change. The top rung stays empty until a named human reviewer has tried to break the work and said so. No amount of computation moves it, by design.
Five fields were scoped and an occupancy check killed or demoted four of them within the hour — the stated hope, and the only reason the exercise was worth running. It asked one question: not whether these fields are new (none are), but whether certified results already exist in them. Certified robustness for ReLU networks turned out to be published under the name min-max representation — the same object as the tropical form, in a paper a search for “tropical” never surfaces. The geometric-algebra one died on its own premise: an interval rotor is a set, and a set cannot satisfy R R† = 1 exactly, so the word carrying the proposal cannot survive contact with interval arithmetic. Both are dropped.
What replaced them was not a sixth field. All five bet on ground being empty, which is the fragile kind of bet — one search settles it. The direction below bets on ground already held.
A point-certificate answers “a solution exists within radius r, and is unique there” — already a geometric hedge. When enough agents interact the answer stops being a point: a coupling that is monotone but not strictly gives a positive-dimensional face, and a non-monotone one gives components far apart. Three results in this programme already exhibit exactly that, at three different rungs — two solutions proved distinct in disjoint balls; a Wardrop split demonstrated to move by ~5.9 while its totals hold to 6.8e-14; and a refusal wall measured in parameter space.
The load-bearing idea: the Wardrop case does not merely fail to certify — it fails in a named direction, one lying in the null space of the Jacobian, which at a solution is tangent to the solution set. So the refusal is not an absence of information; it is the instrument reporting where the set extends. If that holds, the contribution is not a better certificate but reading an existing certificate's failures as data.
The one survivor of the five, and the tiering is strict. A computable a posteriori bound is folklore — weak duality gives it in a line. Rigorous enclosure of the discrete value is occupied, with a 2004 date. What remains is a validated enclosure of a continuous object carrying the discretization error — and that clause is load-bearing: strip it and the claim collapses into folklore plus prior art. This programme already certifies the discrete case by zero-gap duality; the open step is the enclosure and the continuum.
Each direction below went through a formal literature pass before any prose was written. The kills are listed with the kills — the base rate is the most useful number on this page. Every idea that was a new model or a new economic insight was pre-empted. The only slots that came back empty were verification slots.
| idea | verdict | who was there first |
|---|---|---|
| pathwise invariant in the common-noise model | PRE-EMPTED | the source paper’s own §3.1 |
| structure of a routing duality gap | PRE-EMPTED | Cominetti–Dose–Scarsini, Math. Prog. 2021 |
| certifying monotonicity by sums of squares | PRE-EMPTED | Leon–Sakos–Sim–Varvitsiotis, NeurIPS 2025 — one month earlier |
| conservation laws / first integrals in MFG | PRE-EMPTED | Kozlov; Gomes arXiv:1704.07209 |
| exact welfare-gap identity for a groundwater commons | PRE-EMPTED ×3 | Gisser–Sánchez 1980; Carmona–Graves–Tan 2018; Cardaliaguet–Rainer, SICON 2019 |
| exploitability as a certificate | SETTLED | MF-OMO — Guo, Hu & Zhang, SICON 62(1) 2024 |
| exact / SOS / modular certificates | SETTLED | Peyrl–Parrilo; Dumas–Kaltofen; Otti |
| interval-certified network equilibrium, as a method | PARTIAL | Kubica–Woźniak; Alefeld; Klimm–Warode — instance survived, method did not |
| an algebra of test-battery completeness | PRE-EMPTED | analog-circuit testability theory, 1989 |
This Laboratory is the continuum complement to finite-state work (MFGLib / MF-OMO): HJB/Fokker–Planck on a grid, a network VI, and interval enclosures — certificates earned instance by instance.
No validated-numerics result for MFG / HJB / FBSDEs / differential-game Nash yet. Conjecture: monotonicity supplies what coercivity supplies elsewhere. Wardrop is the finite-dimensional rehearsal.
“The mean-field solution is an ε(N)-Nash of the N-player game” is stated with a generic constant. Publishing the first evaluated constant — even if pessimistic — is still the paper.
Testing a solver against random polynomial manufactured solutions is PIT — Schwartz–Zippel detection bounds for code correctness. No connection between the two literatures appears to exist.
The ask. All three need monotonicity theory on one side and verification engineering on the other. Nearest O1 target: a mean-field price-formation model with theorems already proved. Batteries, failure log, and literature kills are available — get in touch · failure log · Laboratory.