Carlos Toledo · reports

Reports

86 reports in five series: audits of machine-generated mathematics, evaluation whose ground truth is a proof, the theorems and exact values that calibrate the instruments, certified decisions for operations, and the record. Each title names the object and what was decided. Each page recomputes its numbers from the certificates and records it cites, and its red controls must fire before it is published.

series 1 · 32 reports

Audits of machine-generated mathematics

Claims produced by AI systems and autonomous discovery platforms — releases, registries, manuscripts, announced records — re-decided from their published bytes, by programs that share no code with the claimant.

audit · AI-discovered algorithms · 2026-08AlphaEvolve and AlphaTensor matrix multiplication, 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 erdős #1 · the disproof made effective · 2026-08Erdős #1: the Astra disproof made effective, with explicit setsGPT-6 Astra disproved Erdős’s first problem in Lean — for every ε there are sum-distinct sets with N ≤ ε·2^n — but the proof is ineffective at one step and no set below Bohman’s 1998 record was known. That step made explicit (a Hermite basis, a chain perturbation, one computed buffer), the sets shipped with certificates, every one re-decided here in exact arithmetic; the base gadget shown not special, and the first explicit Siegel-lemma bounds above Bohman’s.1,701 integers at N/2^n = 0.217967 · 121,500 at 0.136855, 37.7% below Bohman audit · the SOTA table · 2026-08The EinsteinArena SOTA table, decided construction by constructionTogether AI’s repository claims a new state of the art over AlphaEvolve on thirteen problems, each checked by the platform’s own float verifier with tolerances. Twenty published constructions re-decided here in exact and certified-interval arithmetic from their own bytes: sixteen exact witnesses, four witnesses only within tolerance and repaired, every improvement real, one printed digit that is the tolerance’s, and a grid maximum replaced by a certified supremum.20 constructions · 16 witnessed · 4 repaired · 8 of 8 improvements real audit · the Millennium claim · 2026-09The 2026 Navier–Stokes blowup claim: the Lean proof read against its statementOpenAI’s 2026-09-08 proof that a smooth force drives a viscous fluid from rest to infinite speed in finite time — Clay’s breakdown alternatives (C) and (D) — audited without trust and without the priority dispute: the formal statement read against Clay’s wording and Mathlib’s definitions hypothesis by hypothesis, the Lean proof built on a laptop and its axioms asked of the kernel, the paper mapped onto the certificate, the writeup dissected by six readers, every printed identity re-run.statement faithful · built here · one clause of Theorem 1.1 not formal audit · the AI-held record · 2026-08Kissing number in dimension 11: K(11) ≥ 604, one configurationK(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, and EinsteinArena’s headline 604 — NEEDS DATA until its coordinates were published on request, four days after the ledger asked) re-decided here in exact Z[√2] arithmetic from published bytes — and the two platforms’ 604s decided congruent, with a certificate. Since 2026-10-05 also the September wave in dimensions 18 and 25–31: every pair of every published configuration decided exactly.two platforms’ 604s: one configuration, with a certificate erdős #852 · refutation · 2026-08Erdős #852: a published constant refuted at its twelfth digitA 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 decided · polynomial maps · 2026-08Gao's Keller maps and a Markus–Yamabe field, decidedFive new counterexamples to the Jacobian conjecture written with Claude Fable 5's help, and a field on ℝ¹⁴ with every Jacobian eigenvalue −1 and three zeros: decided in exact rational arithmetic from the TeX the papers print, the largest map rebuilt from its construction.8 maps decided · 7 whole, 1 partly, 0 refuted decided · diagonal Ramsey numbers · 2026-08Diagonal Ramsey: the Gupta–Ndiaye–Norin–Wei iteration, certifiedGupta, Ndiaye, Norin and Wei print one more round of their optimisation, proposed by ChatGPT 5.6 Sol, as preliminary and unverified. Decided on their own Theorem 14 by two independent programs: it holds (3.7823). Five further rounds, each in the region the last establishes, reach R(k, k) ≤ 3.7721^(k+o(k)).CERTIFIED · two programs · c = 3.7721307629… after 6 rounds · one-file verifier audit · a benchmark's discoveries · 2026-09HorizonMath's discoveries, decidedA benchmark of unsolved problems credits frontier models with six discoveries and prints three. The Kakeya area holds, exactly; the certificate for a better diagonal-Ramsey base does not satisfy the theorem it is applied to — its checker admits pairs the theorem's region cannot contain, and the certificate uses one where the constant is read.3 credited results decided · 1 certified, 1 refuted, 1 needs data audit · OpenAI's math release · 2026-10OpenAI's math release: what it claims beyond what it checksOpenAI's 719 machine-generated manuscripts and 416 Comparator challenges, audited three ways — a second kernel, every Lean statement read against its claim, every finite witness re-decided exactly — and the gaps between what is claimed and what is checked, ranked and pinned to file and line at the commit audited, found before any fix.14 gaps found 2026-10-10 · 34 of 242 formalized families short of their claim · nothing refuted audit · the constants registry's PR queue · 2026-08Five pull requests to the constants registry, decided where decidableTao's optimization-constants registry has fifteen open, mostly machine-assisted pull requests and no review since September. Five read from their submissions: two exact step functions tightening C₁a and C₁b, a two-law entropy certificate for C₃c, five one-line bounds, OpenAI's Borsuk counterexample, and a de Bruijn–Newman "certified record package" at 0.1595 whose scorer compares rationals and hashes while its analysis cites a bank outside the bundle — every finite object holds, the proofs read hold, the package is refused.9 certified · 1 refused · C₁a ≤ 1.5027435 · C₃c ≥ 1.674894 · Λ ≤ 0.1595 refused audit · five Graffiti.pc conjectures · 2026-08Written on the Wall II: five counterexamples, decidedOne account filed sixty Graffiti.pc conjectures with disproofs on formal-conjectures in a day. The five with explicit witness graphs — total domination in trees, 2-domination in bridged cliques — rebuilt from the author's own Lean tables and decided in exact arithmetic from the archive's definitions: all five refute their conjectures by the stated margins; two notes on the Lean statements; the cited fork commits vanished the same evening, the copies decided are pinned.5 of 5 witnesses certified · trees of 25, 41, 150 vertices · clique graphs of 39 and 15 audit · a peer-reviewed release, replayed · 2026-08AlphaProof Nexus: the proofs hold under two kernels; three OEIS conjectures were already proved, and two statements are degenerateGoogle DeepMind’s AlphaProof Nexus (Science, October 2026) reports 9 of 353 open Erdős problems resolved and 44 OEIS conjectures proved, “correctly formalized and previously unproven”. Every published Erdős proof, and the corrected #741(i), checked by Comparator against formal-conjectures’ own statement and replayed through Lean’s kernel and nanoda: all hold. The nine are seven problems; 38 of the 44 OEIS proofs are published; three of those conjectures already had a proof on record, and two statements hold for a reason unrelated to their conjecture.10 proofs certified, two kernels · 38 of 44 OEIS proofs published · 3 already proved · 2 degenerate audit · the NIST curve seeds · 2026-08NIST’s ECDSA curve seeds: the timestamp-and-lrand48 origin, re-decided from the standardsAnthropic’s 16 October 2026 claim that the fourteen NIST and X9.62 curve seeds are lrand48 candidates seeded from 1997–98 Unix timestamps, and that six base points come from FreeLIP’s generator, re-decided the same evening from the POSIX, X9.62/FIPS 186-2 and FreeLIP specifications by two deciders sharing no code with each other or with the claimant: every checkable row holds, FIPS’s own printed intermediates reproduced; the skipped candidates, the probabilities and "less plausible" listed as readings.34 of 34 checkable rows certified · 14 seeds, 14 derivations, 6 base points · 12 red controls · 6 readings audit · a registry's unanswered claims · 2026-08The AlphaEvolve repository's community certificates, decidedEight issues on DeepMind's repository of problems offer explicit objects beating its recorded bests — sphere-free grid sets to n = 40, two 58-point isosceles-free sets where the literature says 56 is optimal, ring loading at 47/42 and 9/8, a sum-difference set past Penman–Wells — most found by language-model searches, none answered. Every finite object decided here in integers from the notebooks' definitions; the two claims with nothing finite to decide refused and named.70 claims certified · 2 refused · C(40) ≥ 104 · C(32) ≥ 58 · 9/8 audit · a disproof of an open problem · 2026-08Bandeira's Open Problem 0.2(a): the disproof, decidedAn autonomous research system published a disproof of Bandeira's matrix AM–GM problem at n = 5 — an exact rational Farkas certificate for Lai–Lim's semidefinite program and a Lean proof. The finite core re-decided here with a certificate of our own, in exact rationals; the claimant's certificate decides the program its code wrote, without the polynomial transposes that make the Gram form a sum of squares, and the two programs agree in floating point on every case — the conclusion stands, the gap sits exactly where the paper declares its boundary.5 of 5 rows certified · our certificate: denominators ≤ 9,970 · the claimant's holds for its own program only audit · AI-found counterexamples · 2026-08Sra's library of AI-found counterexamples, decided case by caseSuvrit Sra's open library of counterexamples, most found by language models, decided case by case by programs that read the published certificate and never the authors' checker: every case's mathematics holds where it can be decided, some rest partly on what no finite computation reaches, one holds under only one of the two definitions its own text gives — and none of the authors' checkers reads the certificate it publishes.14 cases decided · 9 whole, 5 partly, 0 refuted audit · the registry's asterisks · 2026-08The optimization-constants registry: five asterisked bounds replayedThe optimization-constants registry marks a bound with an asterisk when its verification is at minimal levels. Three hold as printed (C3b, C3c, C71); C42 holds in its limiting inequality, the rest an argument in prose; C84b <= 1.999281 quotes a constant its source only suggests and cannot reach, and holds as 1.9993 — and the checker published with C3c prints OK for a false bound.3 certified · 1 partly · 1 repaired · 1 checker that compares in doubles audit · standing registry · 2026-08The Ramanujan Machine's continued-fraction sheets, 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 · both walls · 2026-08The rank of 3×3 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 quotes · 2026-083×3 matrix multiplication: the 55-addition claim re-derivedEveryone 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 audit · six AI-claimed theorems · 2026-08Six AI-assisted results re-verified from their manuscriptsSix 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 only · 2026-08Maxwell's point-charge bound: the 24-critical-point configuration 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 criterion · 2026-08The Korenblum constant c₂ ≥ 0.4263: re-verified from the manuscriptc₂ ≥ 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 fragment · 2026-08Erdős #1038, the Darvas–Peng–Tao value: the computational fragment 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 only · 2026-08Ran–Teng Conjecture 20: the machine-checkable fragment 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 only · 2026-08The Mathieu property for Lie groups: supporting identities 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 counterexample · 2026-08The rank-two Poisson conjecture: the explicit counterexample 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 counterexamples · 2026-08Eleven Jacobian and Hessian counterexamples, decided exactlyThe 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 negatives · 2026-08The impostor catalog: published constants that match closed formsPublished 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 audit · ζ(3) sheet · 2026-08The Ramanujan Machine's ζ(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 audit · a ζ(7) proof · 2026-08A claimed proof that ζ(7) is irrational, auditedAnand’s preprint audited in exact arithmetic: its outer integral, recomputed from its own formulas, is positive, so A₂₀₀ + U, which must be negative, is positive under every reading and every decided repair. The third-party report that found it is right on every point checked. The proof fails; ζ(7)’s irrationality is untouched.I_out = +1.5757 (printed −15.28) · A₂₀₀ + U = +NaN where the proof needs < 0 (printed −11.99)

series 2 · 10 reports

Evaluation whose ground truth is a proof

Graders measured against provably wrong answers, answer keys re-decided, and environments and benchmarks in which a certificate replaces the answer key.

the eval · live board · 2026-08The 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 · the time horizon · 2026-09METR's time horizon, re-derived as certificatesThe headline number of frontier-AI forecasting — the length of task a model completes half the time — is a logistic fit read at one half. Here every such fit on METR’s own Time Horizon 1.1 evidence is proved to hold exactly one optimum in a box narrower than a trillionth, the horizon is an enclosure over that box, METR’s printed coefficients are its rounding for 22 of 23 models, its point estimates sit within a solver’s tolerance of it, and the post-2023 doubling time re-derives as 128.74 days to the printed digit. The instrument built to decide a time horizon on tasks with no judge in the loop, calibrated on the one that exists. audit · the answer key · 2026-09GSM8K's answer key, re-decidedThe grade-school math benchmark every harness scores against a stored answer line: all 4,282 calculator annotations of the test set and 23,716 of the train set evaluated exactly from the expression they print, every readable prose equation with them, each item classed by whether its own arithmetic reaches its own answer, and the whole read against GSM8K-Platinum’s human revision. The arithmetic is clean where the humans looked and slips where no model disagreed; the ten relabelled answers are readings, not sums. verified reward · demo · 2026-08The verified reward channel in closed 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 · forecasting · 2026-08The Forecast Gym: a forecasting eval 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 builders · 2026-08When the answer key is wrong: three certified specimensThree 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 installable · 2026-08break-the-grader: an RL environment with no answer keyA 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 benchmark · pre-registered · 2026-08Certified MathBench v0: three models on 46 constructions, decided exactlyThree Claude models asked, once each, for 46 constructions in seven families — rulers, caps, codes, graphs, laws, sphere packings, bilinear algorithms — every answer decided exactly, no answer key and no judge, under a pre-registered ceiling.certified: Haiku 5, Sonnet 18, Opus 21 of 46 · US$22.30 environments · the grader, graded · 2026-08Tolerance graders measured against provably wrong answersA 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 eval note · alignment sandbox · 2026-08Scoring AI-generated science: a certificate, not a scoreAn 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

series 3 · 28 reports

Theorems and exact values

Results proved here in exact rational or outward-rounded interval arithmetic — the calibration of the instruments, and some values that were not known.

erdős #1186, k = 3 · a theorem · 2026-10δ₃ = 117/2192: the twelve-block colouring is optimalHow few monochromatic progressions a, a+d, a+2d can a red–blue colouring of 1, …, n have? Since 2008 the answer was known to lie between 0.05112·n² and 0.05338·n², the upper end a colouring in twelve blocks conjectured optimal. It is: δ₃ = 117/2192. Two pages of mathematics and five exact certificates, made in a sandbox and re-decided here by a second verifier that shares no code with the first. Not refereed, not formalised; k ≥ 4 untouched.5 certificates verified twice · smallest margin 2.75e-4 · 5 regions cover [0, ½] erdős #1038 · the infimum, bracketed · 2026-08Erdős #1038: a certified unconditional bracket for the 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 · 2026-08Chowla's cosine problem: λ(5) = −L(1,2,4,5,6), and λ(6) < λ(5)The 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 · 2026-08Chowla's cosine problem: λ(4) = −L(1,2,3,4), provedThe 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 certified theorem · hot spots · 2026-09Hot spots on a convex trapezoid: the extrema stay 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 splitting · 2026-09Congestion mean-field games beyond the uniqueness wall: certified splittingA 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 erdős #1038 · the supremum side · 2026-09Erdős #1038, supremum side: Tao's theorem re-decided degree by degreeTao 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 generation · polynomial multiplication over F2 · 2026-08Polynomial multiplication over F₂: a certified search against the 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 data · 2026-08Erdős #852: the conjectured constant c₀ against the OEIS recordErdő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 measured · ζ(5) → ζ(7)? · 2026-08The Hankel-determinant method past ζ(5), measuredThe Hankel-determinant method behind the September 2026 proof that ζ(5) is irrational, computed exactly past it: every polynomial content-stripped to the smallest one the proof can use, its true margin ball-certified. ζ(3) and ζ(5) clear zero; ζ(7) and Catalan’s G do not in any of 323 families, and the exact p-adic content shows why. The wall is a measurement, not a theorem; the race claims are labelled unverified.ζ(3) −1.38 · ζ(5) −0.19 · ζ(7) +1.02 · G +0.43 · 51/51 re-run rows agree lab · the plane, decided · 2026-08The MFG regime observatory: the coupling–potential plane decidedThe 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 populations · 2026-08A two-population mean-field game: the coupling plane decidedThe 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 · multiplicity · 2026-08A non-monotone mean-field game: two equilibria, certified in disjoint ballsCertified 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 · registry · 2026-08The MFG laboratory: a published Wardrop table reproduced and provedThe 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 erdős #510 · certified landscape · 2026-08The Mercer program: Chowla's cosine problem and Newman's minima, certifiedChowla’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 · theorem · 2026-08Erdős #290: the 4k(k+1) law as exact integer identitiesThe 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 certified invariant · 2026-08The Hénon map: a certified lower bound on topological entropyA 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 erdős #1038 · verification · 2026-08Erdős #1038: thirty published decimals verified, the last a roundingThe 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 validated numerics · the measurement · 2026-08The congestion-MFG certifier's frontier, measuredWhere the congestion mean-field-game certifier stops certifying as the crowd concentrates, at six viscosities and four truncation orders: the boundary of a fixed-order certificate moves with the order, and an N-free ceiling read off the code does not. A lower bound, said so.pinned data re-derived at build interval arithmetic · the replication · 2026-09The Ashrafyan–Gomes error tables, re-decided cell by cellThe two error tables of the Ashrafyan–Gomes semi-Lagrangian scheme met by intervals: the analytic solutions enclosed, the scheme rewritten from the paper, every printed cell given a verdict — the price column reproduced to its digits, the tolerance found inside the finest number, and the printed density found not to be one.record re-derived at build validated numerics · the atlas · 2026-09The p-Laplacian regularization of a first-order MFG, measuredFerreira, Gomes and Üçer restore coercivity with a p-Laplacian to prove that first-order mean-field games have solutions. On the one-dimensional game every regularized equilibrium and the unregularized one are enclosed, cell by cell across an atlas, and the distance between them is decided: the regularization was for the proof; the equation was elliptic all along.record re-derived at build interval arithmetic · the band · 2026-08The effective Hamiltonian of a one-dimensional MFG, enclosed as a bandThe one-dimensional effective Hamiltonian of the cell problem enclosed as a band: flat exactly, rotating bracketed, the threshold enclosed and the point inside it left undecided, the Mather measure decided where it rotates; Gomes–Yang's tables held against it and the eight-digit value they quote found one digit too generous.record re-derived at build validated numerics · the grammar · 2026-09The Gomes–Üçer maximal value function, enclosedGomes and Üçer prove that a first-order game’s value function is decided only where the density lives and is one of many where it does not. An explicit game with a vacuum, built here, shows it: the maximal solution enclosed cell by cell, the chosen one dotted beneath it, the gap between them proved.record re-derived at build validated numerics · the flow · 2026-08A monotone mean-field-game flow, provably not a gradient flowTwo certificates on one MFG equilibrium: the Lasry–Lions form is c∫δm² + ∫m(δu′)² exactly, and the monotone flow of the Gomes school has a certified non-real eigenvalue there — not a gradient flow under any metric. Two instances honestly undecided.record re-derived at build validated numerics · the grammar · 2026-09A first-order mean-field game with entry and exit: the empty region decidedAlharbi, Ashrafyan and Gomes’s first-order game with an entry and an exit: the region where the density vanishes decided cell by cell, refused on the cells holding the free boundary, the two value functions enclosed, and contact without exit evaluated as an interval.record re-derived at build validated numerics · first order · 2026-09The Almulla–Ferreira–Gomes game: the case without a closed form, enclosedAlmulla, Ferreira and Gomes say of their nonzero-drift case that no closed form is known. The game reduces through its constant current to two numbers, enclosed in a Krawczyk box with every integral rigorous; the paper’s own closed form is the control.record re-derived at build validated numerics · 2026-08A 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 reproduction · 2026-08A Wardrop equilibrium enclosed, not only converged toThe 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

series 4 · 10 reports

Certified decisions for operations

Engineering and operational numbers decided over declared envelopes: aviation, maritime, energy, ocean statistics. Each page names what it does not claim. The products built on these decisions are listed at /apps/.

finance · Tesouro Direto, every price · 2026-10Tesouro Direto prices re-decided from the official rule tableEvery fixed-rate Tesouro Direto price since 2004 re-decided from the Treasury’s own rule table in exact arithmetic — the settlement and rounding conventions measured, every OFF price listed with the exact value and the difference in centavos, a second decider sharing no code on every exception.145,439 prices decided · 91.01% the rule’s value to the centavo · 237 off aerospace · the app, cited · 2026-08SkyAudit: one day of New York helicopter traffic, decided flight by flightOne 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 year · 2026-08HarborProof: the EU-MRV fleet under FuelEU Maritime's penalty formulaEvery 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 ocean engineering · the contour benchmark · 2026-09The environmental-contour benchmark, re-decided exactlyNine groups submitted environmental contours — the curve an offshore designer reads a 50-year sea state off — for six metocean datasets, and the benchmark scored each by counting the hourly observations outside it with a float point-in-polygon test. Every submitted contour re-read here as the exact polygon its file denotes and 1.8 million hourly sea states classified inside, outside or on it exactly: 173 of 176 printed counts reproduced to the integer, two traced to a rewritten file, 30 contours that cross themselves, two observations exactly on a contour, and the paper’s expected numbers certified.150 contours · 176 printed numbers · 173 exact ocean engineering · the return-level table · 2026-08Significant-wave-height return levels as certificatesThe extreme-value method of Reis, Guimarães et al. (Ocean Eng. 2026) — six families fitted by maximum likelihood to significant wave height, four goodness-of-fit criteria, block maxima, 100- and 1000-year levels — repeated with every fit certified on three NDBC buoys and on the paper’s own hindcast at 13 grid points. The exponentiated Weibull wins one hourly series of three; on 8 series of 12 the generalized gamma’s likelihood is proved to peak at its lognormal limit. And the Hs marginals the benchmark’s teams printed for the same ten years of one buoy put the 100-year wave anywhere from 5.3 to 14.5 m — one printed row is the fit of the wave period.78 of 90 fits certified · 13 of 15 choices decided ocean engineering · sixteen thousand breakers · 2026-09The geometry of 16,369 Black Sea breaking waves, decidedGuimarães, Stringari, Filipot, Leckler, Benetazzo and Chapron (GRL, 16 September 2026) published the geometry of 16,369 breaking waves filmed in stereo on the Black Sea. Every number the paper prints read against its own table in exact arithmetic — the fitted laws and the 4 % self-similar tail reproduced to the digit, the θ range and the Hs column found to be other columns — and the sea-state stratification the paper leaves undone, done per record.16,369 events · 34.5% in the tank’s band · ρ ≤ 0.41 aerospace · energy certificates · 2026-08eVTOL energy reserves: feasibility certificates under the FAA ruleEnergy-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, decided · 2026-08The engine-out glide ring as a certified bandEngine-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 theorem · 2026-08The water value in a hydro grid: a martingale, proved by LP dualityThe 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 exact arithmetic · the band · 2026-09The Gomes–Saúde electricity price as a proved bandThe Gomes–Saúde electricity price closed in exact rationals: a forecast box on the supply becomes a price band that is a theorem — every path inside prices inside, both edges attained — and the source lab's own kernel is found clearing a market whose batteries do not fill.record re-derived at build

series 5 · 6 reports

The record

What was decided month by month, what was refused and why, how to re-run any of it, and how a claim is submitted.

the rerun kit · 2026-08The rerun kit: re-derive any decided claimFor every record the claims register is derived from: the command that re-derives it, the standard-library verifier and the second implementation where they exist, the record's hash at this build — and the registry of who outside has re-run what, the one number that measures the independence this machine claims.25 records · 7 stdlib verifiers · 1 independent rerun recorded the claims desk · 2026-08Submitting a claim for certificationA 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.131 claims decided · 0 submitted so far the monthly ledger · 2026-08Decided, October 2026: the monthly registerEvery published claim decided in October 2026, read from the register: what held, what did not, and what went wrong, in one closed vocabulary — a dated diff of the records, nothing typed.45 decided · 1 with something wrong the monthly ledger · an earlier month · 2026-08Decided, September 2026: the monthly registerEvery published claim decided in September 2026, read from the register: what held, what did not, and what went wrong, in one closed vocabulary — a dated diff of the records, nothing typed.68 decided · 20 with something wrong note · the third verdict · 2026-08Refusals on record, by kindEvery 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 note · 2026-08How the bugs were foundEvery real bug this machine has found, cataloged: ten caught by a red control, a calibration, an impossible number, or a byte pin, and six found on 2026-10-09 by an adversarial read of the code, counted apart. How to build verifiers that catch their own defects, stated as engineering.every regression re-held by a battery at build