cert-machine · reports

The reports

Research notes ordered by weight, not date. Every page re-proves itself: its numbers are recomputed from the certificates and records at build time, its planted falsifiers must fire, and a build that drifts refuses to ship.

the shelf

Verification — the audits, the environments, the desk

the eval · live boardThe matmul eval: ground truth is a proofFrontier models are asked for exact rank-R matmul tensor decompositions; every proposal is certified or refuted in exact rational arithmetic. No judge, no rubric, no answer key to contaminate — a proof either exists or it does not.364 proposals graded · zero subtly-wrong survivors audit · AI-discovered algorithmsThe AI-discovered algorithms, certifiedAlphaEvolve’s rank-48 ⟨4,4,4⟩ certified over Z[i]; AlphaTensor’s rank-47 verified over F2 and REFUTED over Q — the speedup provably requires characteristic 2. Both decided from commit-pinned bytes at every build.10 algorithms re-decided each build audit · the AI-held recordThe kissing ledger: dimension eleven, decidedK(11)’s record moved three times in eighteen months — every mover an AI, each validated by its producer’s own verifier. The whole ladder (AlphaEvolve 593, EinsteinArena 594, the Station’s three exact 604s) re-decided here in exact Z[√2] arithmetic from published bytes; the one claim with no public bytes measured as NEEDS DATA.K(11) ≥ 604 · certified from the claimants’ own bytes verified reward · demoThe verifier in the loopThe reward channel in closed loop: a model proposes, the grader answers every failure with its own refutation mechanism — the exact violated equation, nothing more — and the model retries. Every trajectory rendered from the append-only ledger.feedback template-locked · zero coaching the eval · forecastingThe Forecast Gym: the test set that cannot leakForecasts are sha-committed to an append-only ledger before their outcomes exist and scored afterward with a proper score in exact rationals — contamination impossible by construction, hedging and overconfidence both priced, admission prune-only with an exact binomial certificate.130 forecasts sha-pinned before their targets note · for eval buildersWhen the answer key is wrongThree certified specimens of mathematical answer keys failing in ways reruns and digit cross-checks provably cannot catch — and the working design that removes the answer key altogether.every specimen re-proved at build an environment · published, and installableBreak the grader, or prove it cannot be brokenA reinforcement-learning environment whose adversarial examples are GENERATED from certified enclosures rather than authored: every negative carries a proof, the set is infinite because the parameter space is continuous, and difficulty is one number with a closed form — the band a tolerance grader leaves open, which vanishes exactly when the tolerance drops under half the certificate width. It is on the Environments Hub as carlos-toledo/break-the-grader, which makes it the one thing here a stranger can check in a single command instead of by reading. On the same 120 tasks it separates three frontier models — +0.950, +0.670, +0.317 — and the smallest scores below a one-line blind policy at +0.558, because the blind policy makes no false claims and that model makes 23.v0.1.2 on the Hub · 360 model calls, $1.92 · the reference table needs no key the claims deskSend us a claimA mathematical claim that comes down to finitely many exact arithmetic facts is decided here — certified with a certificate that re-runs without this engine, refuted with the falsifying witness printed, or honestly refused. Every row of the ledger is derived from the record that decided it, the queue is open and its submitted count is published even while it is zero, and the claimant's code is never in the trust path.18 claims decided · 0 submitted so far environments · the grader, gradedWe graded the gradersA grader that checks a number against a stored decimal within a tolerance accepts values that are provably wrong — and a certified enclosure mints those values without limit, so the adversarial set is generated from certificates rather than written by hand. Measured here against the four reference grader shapes, with three environments built on the same primitive: a grader QA suite, a gym where a verdict without evidence scores zero, and one that rewards BREAKING a grader rather than satisfying it.measured offline · every canary traces to a sha-pinned certificate note · the third verdictWhat the machine would not decideEvery refusal on record, by kind, each with its own denominator: the grader's refusal rate on claims other people submitted, the generation loop's own refusals, NEEDS DATA where a claimant published no bytes to decide on, campaigns published as unfinished, and the undecided cells of two exhaustive sweeps. Deliberately no total — the kinds are not commensurable, and one big number would be a smaller fact.no total on purpose · every row names its denominator methods noteNone by reading codeEvery real bug this machine has found — ten, cataloged — was caught by a red control, a calibration, an impossible number, or a byte pin. How to build verifiers that catch their own defects, stated as engineering.every regression re-held by a battery at build audit · standing registryThe Ramanujan Machine, auditedEvery row of all seven published result sheets decided by rigorous enclosures and exact rational comparisons — the whole registry re-certified at every build.51 printed rows · 50 survive · 1 refuted, correction certified audit · six AI-claimed theoremsWe checked the AI's homeworkSix mathematical results produced with frontier-model help — a counterexample to Maxwell's point-charge bound, a new lower bound for the Korenblum constant, an Erdős problem open since 1958 and three more — each re-verified here from the manuscript by verifiers that never ran a line of the authors' code. 5 held, 1 came back PARTIAL, 0 were refuted; in all 6 the computational fragment certified and the analytic core was out of reach.92 checks · 21 mutation controls, all rejected one of six · at ε = 1/6 onlyMaxwell's point-charge bound — re-verifiedFive positive point charges in ℝ³ whose potential has at least 24 nondegenerate critical points — exceeding the conjectured bound of 16. Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.CONFIRMED · 3 mutation controls, all rejected one of six · the numerical criterionThe Korenblum constant — re-verifiedc₂ ≥ 0.4263, via a moment-duality criterion and an explicit rational eight-atom measure (arXiv:2607.17748). Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.CONFIRMED · 4 mutation controls, all rejected one of six · the computational fragmentErdős Problem #1038 — re-verifiedThe infimum is exactly D = 1.834430475762661711090753635125…, in a July 2026 manuscript of Darvas, Peng and Tao. Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.CONFIRMED · 4 mutation controls, all rejected one of six · machine-checkable fragment onlyRan–Teng Conjecture 20 — re-verifiedResolved, in a preprint. Source status: "Human-checked mathematical proof; no formal proof assistant artifact located" (24 Feb 2026). Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.PARTIAL · 5 mutation controls, all rejected one of six · supporting identities onlyThe Mathieu property for Lie groups — re-verifiedExactly the tori — a classification. Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.CONFIRMED · 3 mutation controls, all rejected one of six · the explicit counterexampleThe rank-two Poisson conjecture — re-verifiedAn explicit counterexample: polynomials R, T, D, S in ℚ[x,q,p,z] with prescribed bracket relations. Re-verified here from the manuscript: the verifier's full check ledger as it printed it at build time, the named falsifiers that prove it can fail, and the boundary the audit did not cross.CONFIRMED · 2 mutation controls, all rejected audit · published counterexamplesThe Jacobian conjecture, auditedThe July-2026 announcement that would refute a conjecture open since Keller 1939 — and the literature that followed it within days — decided in exact rational arithmetic: the Jacobian determinant expanded symbolically and compared coefficient by coefficient, every claimed collision re-evaluated as fractions, then the published witnesses thrown away and the collisions found again blind. Eight rows re-certify a sha-pinned published source; three are counterexamples this machine generated itself and no paper carries.11 certificates · 3 generated here, in no paper proved negativesThe impostor catalogPublished constants that agree with simple closed forms for dozens of significant digits — and exact proofs that every one of them is lying. Digit agreement is not evidence: the answer-key-contamination parable.exact BigInt refutations at full published precision eval note · alignment sandboxAlien science needs a dispositionAn evaluation note on Anthropic’s automated-alignment sandbox: its authors name evaluation as the binding constraint, and this is what certified evaluation looks like.posted to the inviting repository audit · ζ(3) sheetThe ζ(3) sheet, decidedThe Ramanujan Machine’s complete zeta(3) result sheet re-decided with certificates: proved tail bands, convergence inside the certificate, exact rational comparisons.the spurious-solution lemma re-proved at build
the open list

Erdős problems, audited

erdős #1038 · the infimum, bracketedA certified bracket for the Erdős–Herzog–Piranian infimumHow small can the set where a monic polynomial stays below 1 be? The infimum is bracketed here in certified interval arithmetic, both ends unconditional — the lower end by a forcing argument needing no tail estimate and no assumed minimizer — and Tao’s model Problem 4.1 is answered affirmatively for every ε. Three AI-assisted proofs of the exact value are currently claimed and none independently examined, so nothing here assumes any of them.1.828 ≤ inf ≤ 1.83443 · both ends certified here erdős #510 · a theoremλ(5), settled — and the sequence turns downThe fourth exact value of Chowla's cosine dip, and the first whose optimiser is not an initial segment: λ(5) = −L(1,2,4,5,6), an algebraic number of degree exactly five, with its minimal polynomial exhibited. One family in the reduction admits no classical weight at all — a structural obstruction the page proves fresh at every build — and a Fejér–Riesz comb gets through it. A consequence needs nothing further: λ(6) < λ(5), so the sequence that had been climbing turns down.theorem audited over 139,246 sets, 0 refuters · the closure trees not yet · not peer-reviewed erdős #510 · a theoremλ(4), settledThe third exact value of Chowla's cosine dip. Mercer proved λ(2) and λ(3) in 2019, conjectured λ(4), wrote that he did not know how to evaluate it, and left a strategy. The machine executed the strategy and finished it: all nine remaining families closed, thresholds derived rather than transcribed, every finite remainder decided in exact arithmetic. λ(4) = −L(1,2,3,4), the root of 512y³ − 1227y² + 600y + 125 near 1.51956 — machine-derived, re-proved at every build, and stated with its verification status beside it.not peer-reviewed · the full record re-derives at build erdős #1038 · the supremum sideHow shallow can a lemniscate stay?Tao reformulated Erdős #1038 over discrete measures and conjectured the supremum of |{U<0}| is 2√2 — "this may be hard to prove completely." For rational weights it is a per-degree polynomial question, and the machine decided the first seven degrees: odd degrees fall strictly below 2.82 < 2√2 (branch-and-bound certificates, 127 boxes for the cubic); even degrees localize the supremum to [2√2, 2.82845] with the two-atom witness within 2.3×10⁻⁵ of optimal. Plus the certified landscape: an interior cubic champion and a quintic cliff where the sublevel set changes topology.per-degree theorems · the conjecture itself stays open · not peer-reviewed erdős #852 · refutationThe constant that was a rounding errorA GPT-published constant on Erdős #852, refuted at its 12th significant digit and shown to BE the naive IEEE-754 float product, digit for digit — with the certified correction, and the failure taxonomy for eval builders.refuted at digit 12 · correction certified audit · both wallsThe rank of 3x3 matrix multiplication, audited from both sidesLaderman multiplied two 3x3 matrices in 23 multiplications in 1976 and nobody has beaten it since. The lower bound moved from 19 to 20 over F2 in March 2026, in a preprint whose proof is a machine-checkable certificate on a two-star repository. Both walls are re-verified here in exact arithmetic, by an instrument built to be able to contradict either.first independent check of the new bound audit · the cost nobody quotesRank is not the cost: checking 55 additions for 3x3Everyone quotes Laderman's 23 multiplications. Almost nobody quotes the additions — and that is where the record has actually been moving, seven times in under a year: 62, 61, 60, 59, 58, 56, and in July 2026, 55. That preprint is a month old and its certificate sits on a repository with zero stars. Every number in it is re-derived here, by an instrument that decides both halves of the claim separately, because a circuit can be short and compute the wrong map or compute the right map and have been miscounted.the claim held; 8 red controls fired generation · polynomial multiplication over F2A free search against forty-year-old multiplication boundsThe best known ways to multiply polynomials over F2 are still hand constructions from 1983 and 2009, and every lower bound underneath them moved in March 2026. A free flip-graph walk was pointed at the gap and certified exactly. It reproduced three published upper bounds from scratch — including the cyclic convolution C7, where the two walls meet, so that rank is the exact answer — and beat none of them. The calibration is the result, and the prior-art check that narrowed the target is on the page.a null result, with the ladder that makes it mean something erdos · conjecture vs dataA conjecture nobody had checked against the numbersErdős #852 conjectures that the longest run of pairwise-distinct prime gaps grows like c₀·log x. This repository certified c₀ to 61 digits; the exact record data has been in the OEIS since 2002; nobody had compared them. Recomputed here in integer arithmetic and placed against the constant — under the reading the problem statement actually gives, they agree across every decade; under the other reading they do not.reproduces every published term, then passes them — a run of 31 pairwise-distinct gaps erdős #510 · certified landscapeThe Mercer programChowla’s cosine dips — Erdős #510 — and Newman’s 0/1 minima certified as one landscape: exhaustive box sweeps, exact champions, a Sturm equality — every claim re-proved at build. The certified lambda table is the note filed on the #510 page.mu(5) ≤ 1 + π/20 · re-certified every build erdős #290 · theoremErdős #290: the 4k(k+1) theoremThe square-discriminant law proved and re-proved as exact integer identities during the build, the enclosure sweep deepened past the cited page, every exceptional degree in range closed.planted falsifiers must fire at build erdős #1038 · verificationErdős #1038: thirty decimals verifiedThe computational fragment of the Darvas–Peng–Tao manuscript re-verified by an independent route — Krawczyk rather than bisection — with the 30th digit read correctly.filed on the claiming authors’ repository

Erdős’s list is a public register of open questions, which makes it the sharpest available test of whether a verdict produced here survives contact with the people who own the problem. Each page decides a finite, exact fragment and says exactly which one: a published constant refuted at its twelfth significant digit with its correction certified, certified extremal tables for Chowla’s cosine problem, a square-discriminant law re-proved as integer identities, and an independent verification of a claimed proof’s computational appendix. What has been filed with each problem, and what has come back, is on the about page, in status words meant exactly.

new fronts

Certified applications with live stakes

aerospace · the app, citedSkyAudit: the helicopter day, decidedOne pinned day of New York helicopter traffic, re-flown on paper by four eVTOLs’ own published numbers under the FAA reserve rule — every flight decided: E-FLYABLE, BEYOND RANGE with an exact witness, or NEEDS DATA where public specs cannot say. The citable methodology behind the live app.every certificate row recounted at the page’s own build maritime · FuelEU, first live yearHarborProof: the fleet, re-sailed under the ruleEvery ship in the official EU-MRV 2025 registry — the first year FuelEU Maritime penalties exist — re-fueled on paper under the regulation’s own published penalty formula, in exact rationals over boxes constrained by each ship’s own reported numbers: penalty floors in EUR, exact zero-WtW blend fractions that flip each verdict, NEEDS DATA where the record’s opacity leaves it open.the whole registry recomputed at the page’s own build aerospace · energy certificatesThe reserve, provableEnergy-feasibility certificates for eVTOL missions against the FAA reserve rule: CERTIFIED for every parameter point in the boxes, REFUTED with an exact falsifying witness, or honestly REFUSED — where the industry argues with Monte Carlo, this decides.verdicts cross-proved by 256-corner exact sweeps aerospace · the ring, decidedThe glide ring is unfalsifiableEngine-out reach on a real pinned single-engine flight, recomputed as an enclosure over the same inputs’ uncertainty: an inner boundary proved reachable, an outer boundary proved not, and the honest annulus between that no shipped product draws. While the panel’s single line sits inside the envelope it cannot be proved wrong about anything — and 57% of what it claims cannot be proved right.650 airfields × 288 states, every verdict decided at the page’s own build energy · certified theoremThe water value, certifiedThe shadow price of stored water in a hydro-dominated grid is a martingale between stock-binding events — proved by LP duality on scenario trees, with the solver extracted from the published artifact’s own bytes and 120 random trees re-certified at every build.duality gap ~1e-14 · continuum limit honestly OPEN

Aerospace and energy: domains where the operative numbers are defended by simulation today, and where a universally-quantified certificate — or an honest refusal — is a different kind of statement. Each page names what it does NOT claim.

the proving ground

The instruments, proven on hard classical ground

certified theorem · hot spotsThe hot spot stays on the boundaryNot one domain but a continuum: for every c in [0.845, 0.85] the convex trapezoid A(0,0) B(1,0) C(c,9/10) D(1/4,9/10) has a simple second Neumann eigenvalue whose eigenfunction attains its extrema on the boundary only — to our knowledge the first certified hot-spots result for a positive-measure FAMILY, with the original specimen c = 17/20 as its right endpoint. The second Neumann eigenfunction of a convex trapezoid with no symmetry axis — to our knowledge the first certified hot-spots domain outside every analytically proven class (all triangles took Judge–Mondal an Annals paper; lip domains, L-tiled polygons and symmetric quadrangles are the other proven classes, while in high dimension convex sets can FAIL the conjecture, making the planar convex case the live one) — attains its maximum and minimum on the boundary only. Corollary: the hot spot is AT vertex A, and only there. Eight machine-checked records, a cell partition decided in exact rationals, corner coefficients certified at two independent annuli, and red controls that fire. One domain, one theorem, one corollary; the quadrilateral conjecture itself stays open.μ₁ ∈ [12.0209761, 12.0223984], simple · the chain re-runs in ~2 min certified theorems · MFG splittingThe crowd splits — MFG beyond the uniqueness wallA congestion-averse crowd in a single-well cost landscape provably settles into TWO density peaks — or THREE. To our knowledge the first validated-numerics equilibrium enclosures for a mean-field game, and the first whose certified peak count strictly exceeds the potential's wells. Two computer-assisted theorems and a bracket table of certified instances whose enclosure balls fix the exact peak count of the exact solution; the discount-free crossover σ* = 1/(8π²) decided in exact rationals; certified multiplicity where uniqueness theory is silent; an EXACTLY-3 census; the 21,567-cell regime map.two theorems + a bracket table · honest counting, every bound displayed lab · the plane, decidedThe MFG regime observatoryThe coupling–potential plane of a mean-field game partitioned into cells and decided — thousands carry two exact equilibria in provably disjoint balls valid for EVERY parameter in the cell, not merely at a sampled point. The certifier runs in the page, ships as one dependency-free file, and refuses at the bifurcation.the partition’s area identity re-checked at build lab · two populationsThe attack–defense regime mapThe coupling plane of a TWO-population mean-field game, decided cell by cell. The standard sufficient condition for a unique equilibrium turns out to be an order of magnitude conservative — and the attack–defense asymmetry it never mentions is the axis along which a solver stops being able to see the second equilibrium at all.verdicts checked against the one-population lab at zero coupling certified theorem · multiplicityTwo solutions, provablyCertified multiplicity for a non-monotone mean-field game: two equilibria enclosed in disjoint interval-arithmetic balls at one parameter set, in the regime where uniqueness theory is silent — and a proof that REFUSES at the bifurcation.the unit’s battery + six falsifiers re-run at build certified reproduction · registryThe MFG laboratory, certifiedThe single-file MFG laboratory’s certified claims: a published Wardrop table reproduced within its own rounding AND proved (Krawczyk box, exact rational solve), the discrete adjoint identity, and the non-unique split behind unique totals.four of the lab’s own batteries re-run at build certified invariantEntropy, with a certificateA certified lower bound on the topological entropy of the classical Hénon map — covering relations composed to an exact integer spectral argument, calibrated at the full horseshoe.h_top ≥ 0.3017, a theorem validated numericsA congestion mean-field game, enclosedAn equilibrium of a mean-field game with congestion enclosed by validated numerics: an exact solution within an explicit radius, locally unique in the full sequence space.embedded verifier re-run at build certified reproductionWardrop, certified: exact, enclosed, refusedThe multi-population Wardrop equilibria of a published paper reproduced with certificates — exact where possible, enclosed where not, and refused where honesty demands it.embedded verifier re-run at build

These are where the verifiers earned calibration before deciding anything a model produced: a published Wardrop table reproduced within its own rounding and then proved outright, mean-field equilibria enclosed in disjoint balls where uniqueness theory is silent and REFUSED at the bifurcation, an entropy bound calibrated at the full horseshoe. The audits above — and the Erdős pages, whose exhaustive box sweeps are these same instruments — stand on this ground.