Review drafts, built from the records: each number in each manuscript is interpolated at build time from a certificate or ledger in the public repository, and the build refuses when a record no longer supports a sentence. Author lists and roles are to be agreed with the reviewing group; nothing on this shelf has been submitted anywhere.
Each paper has a report page on this site where the same record is recomputed at every build, and a LaTeX source in the repository whose numbers are macros written by a tool from that record (tools/build-paper-numbers.js and tools/paper-numbers/). The prose is authored and should be reviewed like any other; the numbers cannot be typed. "Certified" is used in its mathematical sense only, defined once per paper; the published work of others is re-decided, never corrected. The forms: Elsevier drafts use the elsarticle preprint layout with highlights, keywords and the required declarations; article drafts use the house preamble with theorem environments. A status of "draft v0.1" means the first complete text; "outside audit" means a group with no shared code re-derived the record.
The line the reviewing group works in: the extreme-value method certified on its own hindcast, printed tables decided, the contour benchmark and a breaking-wave dataset re-decided.
| paper | status · links |
|---|---|
| Certified return levels: deciding maximum-likelihood extreme-value fits of significant wave height over a public global hindcast The six-family, four-criterion method of Reis et al. (2026) repeated on its own hindcast with every fit proved the likelihood's one maximum in a box: 46,602 fits over 2,589 cells, 5,751 refused with the proof of a limit; the ten regional claims decided; a library's two answers and a published design table decided. | draft v0.1 · 2026-10-01 · for Ocean Engineering · 29 pp · 1.5 MB PDF · report · source · hseva-atlas.json · hseva-ledger.json · design-table-audit.json |
| Certified return levels — the two-page extended abstract for the agreement of scope Problem, method, results and novelty of the return-levels paper in two pages, ending with the questions the co-authors must settle: the journal, the re-boxing of the ten claims, the GEV section, the Python verifier. | draft v0.1 · 2026-10-01 · for Ocean Engineering · 4 pp · 575 KB PDF · report · source · hseva-atlas.json |
| The environmental-contour benchmark re-decided exactly: 150 submitted contours as exact polygons, 1.8 million hourly sea states classified in exact arithmetic, and the counts the organizers printed The 2021 benchmarking exercise for environmental contours re-decided exactly: each of the 150 submitted contours read as the polygon its digits denote, 1.8 million hourly sea states classified inside, outside or on it with every sign certain, 173 of 176 printed counts reproduced to the integer, two traced to a rewritten file, 30 self-crossing polygons, the expected numbers certified. | draft v0.1 · 2026-10-01 · for Ocean Engineering · 23 pp · 337 KB PDF · report · source · ecbench-ledger.json · claims.json |
| The geometry of 16,369 breaking waves, re-decided in exact arithmetic from the published table, with the sea-state stratification the dataset allows Every number printed in Guimarães et al. (GRL 2026) on 16,369 Black Sea breaking waves, re-derived from the published table in exact arithmetic: the three quadratic laws and the 4% self-similar tail reproduce to the digit, two printed quantities are other columns of the table, and the sea-state stratification the paper leaves open is done per record. | draft v0.1 · 2026-10-01 · for the dataset's authors first · for Coastal Engineering · 21 pp · 351 KB PDF · report · source · breaking-ledger.json · claims.json |
A number a model proposes, decided over the declared uncertainty envelope: three verdicts, witnesses, the threshold that decides.
| paper | status · links |
|---|---|
| A decision procedure for machine-proposed engineering numbers: three-valued verdicts over a declared uncertainty envelope, with witnesses and the threshold that decides A water-injection flowline under Colebrook and Darcy–Weisbach: a plausible +4.2% recommendation refused with inputs at 361.6 and 344.2 bar against a 360-bar rule, proved at a 204-bar discharge; seven injected faults each refuted or refused; Monte Carlo face to face; the same grammar on the hindcast, the library and the design table. | draft v0.1 · 2026-10-01 · for Reliability Engineering & System Safety · 17 pp · 151 KB PDF · report · source · gate-ledger.json · claims-ledger.json |
| Guaranteed 4D seismic detectability of gas and CO₂ injection fronts in a pre-salt-type carbonate: a decision over a declared petro-elastic envelope Gassmann over a declared envelope by interval branch and bound: four proved numbers per cell of a porosity–saturation grid, three verdicts with witnesses, the resolution that decides. On UNISIM-IV at the Tupi pilot's 1.5%: thin fronts proved undetectable in 50,186 cells, the pilot's band refused in four of five knowledge states, the sign of the change not guaranteed above a gas density of about 0.70 g/cm³. | draft v0.1 · 2026-10-01 · rock-physics review pending · for Journal of Applied Geophysics · 19 pp · 248 KB PDF · report · source · decidivel-ledger.json · declared.json |
Results the machine proved or bracketed in exact and interval arithmetic, with the record beside each.
| paper | status · links |
|---|---|
| The value of λ(4): a machine-derived proof completing Mercer's Section-5 program λ(4) = −L(1,2,3,4), the third exact value of Chowla's cosine problem (Erdős 510, finite front), proved by executing and completing Mercer's 2019 reduction with every finite case certified in exact arithmetic; re-certified in September 2026 by an outside group with no shared code (teorth/erdosproblems issue 392). | draft v0.9 · 2026-09-01 · outside audit 2026-09-30 · 8 pp · 416 KB PDF · report · source · lambda4-campaign.json · lambda4-audit.json |
| The value of λ(5) in Chowla's cosine problem, and the Mercer program as a certified landscape λ(5) = −L(1,2,4,5,6) proved by executing Mercer's reduction one level deeper: fifteen discovered conditions, eight families closed as certified trees, a squared-modulus comb past the one cone no classical weight passes, the quintic minimal polynomial, the descent λ(6) < λ(5), an independent walk of 139,246 sets, and the certified μ/λ landscape; λ(6) left open. | draft v0.1 · 2026-10-01 · 14 pp · 172 KB PDF · report · source · lambda56-campaign.json · lambda5-audit.json · lambda-table.json |
| The hot spot stays on the boundary: a certified theorem for a convex trapezoid The second Neumann eigenfunction of a convex trapezoid outside every analytically proven class attains its extrema on the boundary only — a certified six-stage chain (eigenpair enclosure, defect, collar, corners, cross, pointwise band) with exact-rational partition decisions. | draft v0.9 · 2026-09-03 · 13 pp · 150 KB PDF · report · source · ember-theorem.json · ember-eigenpair.json |
| Explicit sum-distinct sets below Bohman's constant: the Erdős problem 1 disproof made effective The GPT-6 Astra disproof of Erdős problem 1 is ineffective at one step; this paper makes it effective and computes the buffer the proof never computed: explicit dissociated sets with 1,701 elements at N/2^n = 0.218 and 121,500 at 0.137, each certificate re-decided in exact arithmetic; the base gadget works for every tilt. | draft v0.2 · 2026-09-16 · certificates archived at Zenodo · 8 pp · 118 KB PDF · report · source · erdos1-ledger.json |
| Certified bounds for Erdős problem 1038, and a tail-free forcing argument The Erdős–Herzog–Piranian infimum bracketed unconditionally, 1.828 ≤ inf ≤ 1.8344305: the upper end replaced by a proof, the lower by a pure forcing argument needing no tail construction; three dual measures verified; Tao's model Problem 4.1 answered for every ε in (0, 0.1]; the forcing method proved exhausted near 1.829. | draft v0.9 · 2026-09-03 · 6 pp · 100 KB PDF · report · source · erdos1038-inf.json · erdos1038-forcing-1.828.json |
| A certified lower bound on the topological entropy of the classical Hénon map: covering relations composed to an exact integer spectral argument The Hénon map at a = 1.4, b = 0.3: a certified lower bound h_top ≥ ln(338,518,196,978)/88 > 0.301680 from 340 disjoint h-sets and 4,140 covering relations decided as strict interval inequalities, chained to the uniform iterate F^11 and bounded by an exact integer row-sum argument; calibrated at the full horseshoe; two verifier defects named, the interim 0.356403 withdrawn. | draft v0.1 · 2026-10-01 · the published rigorous bounds are stronger; the grammar and the record are the claim · 12 pp · 214 KB PDF · report · source · entropy-henon.json · census-high-periods.json |
| The supremum side of Erdős problem 1038: per-degree certificates for the 2√2 bound, and the thirty published decimals of the infimum verified Degrees 3 to 8 of the supremum side of Erdős problem 1038 decided in exact arithmetic, independently of the December 2025 proof that the supremum is 2√2: odd degrees strictly below 2.82, even degrees localized to [2√2, 2.82845], degree 9 refused, the family landscape certified; and the thirty printed decimals of the Darvas–Peng–Tao infimum constant verified against a Krawczyk enclosure, the last one a rounding. | draft v0.1 · 2026-10-01 · reframed: re-decisions of a known theorem · 12 pp · 157 KB PDF · report · source · sublevel-tao179.json · erdos1038-inf.json |
| Erdős problem 290: the 4k(k+1) square-discriminant law as exact integer identities, and a certified bracket for the Galois-density constant behind both endpoints of van Doorn's Theorem 8 Erdős problem 290: the discriminant of the derivative of x(x−1)⋯(x−d) is a perfect square exactly at d = 4k(k+1), proved and checked as exact integer identities; the Galois density decided at every even d ≤ 620; a certified bracket for van Doorn's constant, 1/(1+c) = 0.546…, three unconditional decimals of a liminf now known exactly. | draft v0.1 · 2026-10-01 · 12 pp · 184 KB PDF · report · source · erdos290-tail-ext.json |
| Erdős problem 852: a published constant refuted at its twelfth digit and identified as a floating-point product, the certified correction, and the record data nobody had compared Two language-model constants posted on the Erdős 852 thread are replaced by certified enclosures: c₀ to 61 decimals (uniqueness proved), C* to width 3.2×10⁻¹⁶. The posted C* is refuted at its twelfth decimal by one exact integer inequality and shown to be the naive IEEE-754 product; an exhaustive scan to 5×10¹¹ extends the OEIS record data and is compared with the conjecture. | draft v0.1 · 2026-10-01 · 12 pp · 163 KB PDF · report · source · erdos852-certificate.json · erdos852-h-records.json |
| Gain-weighted well-counting in a congestion mean-field game Certified equilibria of a stationary discounted congestion mean-field game on the torus whose density carries more local maxima than the potential has wells: exactly two over one well, exactly three at a third-harmonic instance, a six-row bracket table pinning the splitting threshold, and the crossover σ* = 1/(8π²) decided γ-free as an exact-rational identity. | draft v0.3 · 2026-10-01 · LaTeX from the markdown draft, the record winning over its rounding · 11 pp · 144 KB PDF · report · source · terra-bracket-table.json · terra-sigmastar.json · mfg-cap-multiplicity.json |
| Certified multiplicity maps of stationary mean-field games: 19,800 and 21,567 parameter cells decided uniformly, two equilibria in provably disjoint balls, and a monotone flow that is not a gradient Two parameter maps of stationary mean-field games on the torus, 19,800 and 21,567 cells each decided over its whole rectangle: two equilibria in provably disjoint balls, unique on the cited monotonicity theorem, or undecided with the reason kept; with three disjoint solutions at six couplings, an exact Galerkin count, a certified non-real eigenvalue of the monotone flow, and where the certifier stops. | draft v0.1 · 2026-10-01 · 15 pp · 262 KB PDF · report · source · mfg-regime-map.json · mfg2p-regime-map.json · mfg-cap-multiplicity.json · monoflow-spectrum.json |
| Published mean-field-game numerics, re-decided: error tables, closed forms, effective Hamiltonians, value functions, regularizations and prices as certified objects Eight published pieces of mean-field-game numerics — two error tables, a benchmark closed form, an effective Hamiltonian and its quoted values, a maximal value function, a regularization atlas, a Wardrop table, a clearing price and an empty region — met by interval enclosures and exact rational decisions, each verdict read from a public record re-derived at every build. | draft v0.1 · 2026-10-01 · 14 pp · 237 KB PDF · report · source · agtable-redecided.json · afg-enclosure.json · hbar-band.json · regatlas.json · price-band.json |
Published AI-era claims re-decided from their own bytes with no code shared with the claimant: certified, refuted with the witness, or refused with the reason.
| paper | status · links |
|---|---|
| Independent exact certification of machine-generated mathematics: the first register The method paper of the project, with its evidence: a register of 88 published machine-generated claims decided in exact arithmetic with no code shared with the claimant — 63 certified, 2 refuted, 10 partial, 5 mixed, 5 repaired, 2 needing data, 1 queued. The grammar of verdict, witness and refusal, the discipline that keeps counts honest, three worked rows, and what the defect kinds measure. | draft v0.1 · 2026-10-01 · the method paper · 15 pp · 182 KB PDF · report · source · claims-ledger.json |
| The diagonal Ramsey iteration of Gupta, Ndiaye, Norin and Wei, verified and continued: R(k,k) ≤ (3.77213…)^(k+o(k)) conditional on their Theorem 14, and a benchmark certificate refuted The "preliminary, unverified" third round of Gupta–Ndiaye–Norin–Wei's diagonal-Ramsey iteration is decided on their own Theorem 14 by two independent interval programs: the printed 3.78233 holds. Five further rounds, each decided in the region the one before establishes, reach R(k,k) ≤ (3.77213…)^(k+o(k)), conditional on the paper. HorizonMath's 3.6961 certificate is refuted: its pair at λ = 1 lies outside the theorem's region, admitted by a one-sided checker. | draft v0.1 · 2026-10-01 · 13 pp · 216 KB PDF · report · source · gnnw-certificate.json · gnnw-chain-certificate.json · horizonmath-ledger.json |
| Explicit counterexamples to the Jacobian and Hessian conjectures, and weak Markus–Yamabe fields, decided in exact rational arithmetic The July–August 2026 refutations of Keller's Jacobian conjecture, Meng–Yang's five-variable Hessian counterexample, Gao's five further Keller maps and the weak Markus–Yamabe fields in dimensions 14 and 18, re-decided in exact rational arithmetic with no code shared with any author: eleven certificates plus eight ledger rows, collisions re-found blind as Krawczyk boxes, partial verdicts and open questions stated as such. | draft v0.1 · 2026-10-01 · 14 pp · 196 KB PDF · report · source · keller-certificate.json · polymaps-ledger.json |
| AI-era matrix-multiplication records, decided from their bytes: AlphaEvolve, AlphaTensor, the EinsteinArena table, the 3×3 addition count and the rank walls The AI-era matrix-multiplication records re-decided in exact arithmetic from pinned bytes: AlphaEvolve's rank-48 certified over Z[i], AlphaTensor's rank-47 certified over F2 and failing over Q, both walls of the rank of 3×3, the 55-addition circuit gate by gate, a free flip-graph walk over F2, and the EinsteinArena table read as the exact rationals its decimals denote. | draft v0.1 · 2026-10-01 · 14 pp · 185 KB PDF · report · source · strassen-certificate.json · easota-ledger.json · bilinear-certificate.json |
| Digit agreement is not evidence: an impostor catalog of published constants refuted in exact arithmetic, and the Ramanujan Machine's printed sheets re-decided Five published OEIS constants agree with simple rationals for 16 to 62 significant digits and are refuted, all 21 spellings, by one integer inequality at the full published length. The Ramanujan Machine's seven result sheets are re-decided as a standing registry: 50 of 51 printed rows survive at certified widths; one is refuted as printed, its sign-corrected identity surviving on the same enclosure. | draft v0.1 · 2026-10-01 · 14 pp · 223 KB PDF · report · source · oeis-constants.json · PINS.json |
| An audit of the 2026 Navier–Stokes finite-time blowup claim: the formal statement read against Clay's wording and Mathlib's definitions, the Lean proof built and its axioms asked of the kernel, and what remains open OpenAI's 2026-09-08 Navier–Stokes blowup claim audited from a digest-pinned corpus: the formal statement read hypothesis by hypothesis against Clay's wording and Mathlib, the 618,762-line Lean proof built on a laptop with its axioms asked of the kernel, the paper mapped onto the certificate, six readings consolidated, every printed identity re-run. Register verdict PARTIAL: the finite-energy clause is not formal. | draft v0.1 · 2026-10-01 · a note · 11 pp · 164 KB PDF · report · source · audit.json · build.json · claims-ledger.json |
| Two platforms, one configuration: independent exact certification of the dimension-eleven kissing records Two AI platforms announced K(11) ≥ 604 four months apart; every public witness re-decided in exact arithmetic over Z[√2] with no code shared with either producer. The two headline configurations are congruent — a signed permutation of the coordinates, with its certificate; three others are pairwise non-congruent by exact contact counts. | draft · 2026-09-08 · 4 pp · 75 KB PDF · report · source · kissing-ledger.json · kissing-congruence.json |
Graders graded, answer keys re-decided, a benchmark pre-registered.
| paper | status · links |
|---|---|
| Certificate-grounded evaluation: when the answer key is a proof — graders graded, answer keys re-decided, a time-horizon fit certified, and a pre-registered benchmark Where a certificate exists, a tolerance grader's accepted-but-wrong band has a closed form, 2·tol − w, and tightening the tolerance provably does not close it. Four results from public, re-runnable records: a canary factory that grades graders, three answer-key specimens and a control, GSM8K's key re-decided to the last step, METR's time-horizon fits certified, plus a verified reward channel and a pre-registered benchmark. | draft v0.1 · 2026-10-01 · consolidates the two earlier markdown drafts · 18 pp · 223 KB PDF · report · source · envs-record.json · gsm8k-ledger.json · horizon-ledger.json · mathbench-ledger.jsonl |
Superseded or being consolidated into the papers above; kept for the record.
| paper | status · links |
|---|---|
| Certificate-grounded grading: a construction manual (sections 1–3 and 7) The markdown draft that the evaluation paper consolidates: verifier false-accept rates measured against labels and adjudicators, and the construction of a proved negative set from a certified enclosure. | draft · 2026-09-16 · being consolidated · markdown, no PDF report · source · envs-record.json |
| A verified reward oracle for AI mathematical search The August 2026 draft on the matmul reward channel: certified, refuted with the violated equation, or refused; screens prune and never admit; the design discipline as the contribution. | draft · 2026-08-27 · being consolidated · markdown, no PDF report · source · matmul-eval-ledger.jsonl |
Read the PDF; where a number looks wrong, open the record it names — the manuscript cannot say what the record does not. Comments on prose, framing, missing literature and venue are what these drafts need most. The repository is public; the drafts are rebuilt with make papers.