Six mathematical results produced with help from frontier AI systems — a counterexample to Maxwell's point-charge bound, a new lower bound for the Korenblum constant, an Erdős problem from 1958, and three more. Each one was re-verified here in exact arithmetic, from the manuscript, by verifiers that never ran a line of the authors' code. This is what survived.
| claim | AI system | verdict | scope of that verdict | named checks | its own total | controls |
|---|---|---|---|---|---|---|
| Maxwell's point-charge bound | OpenAI GPT-5.6 Sol (idea) | CONFIRMED | at ε = 1/6 only | 17 | 20 | 3 |
| The Korenblum constant | OpenAI Codex (GPT-5.6 Sol), disclosed in the paper | CONFIRMED | the numerical criterion | 15 | — | 4 |
| Erdős Problem #1038 | GPT-5.5 Pro (initial main argument in a solver–verifier framework, then revised by the human authors) | CONFIRMED | the computational fragment | 22 | 26 | 4 |
| Ran–Teng Conjecture 20 | GPT-5.2 Thinking | PARTIAL | machine-checkable fragment only | 38 | 43 | 5 |
| The Mathieu property for Lie groups | not recorded at source | CONFIRMED | supporting identities only | — | 126 | 3 |
| The rank-two Poisson conjecture | not recorded at source | CONFIRMED | the explicit counterexample | — | — | 2 |
The six verifiers do not agree about what a check is, and the two columns say so rather than hiding it. Maxwell, Ran–Teng and Erdős #1038 fold their mutation controls into their own printed total (17+3=20, 38+5=43, 22+4=26); Mathieu counts its controls separately; Korenblum and Poisson print no total at all. So the first column is computed here by ONE rule applied to all six — a named check row that is not a mutation control — and the second column is whatever each verifier says about itself. Where a verifier names no rows, or states no total, the cell reads — instead of a number we invented. Click any claim for its full ledger.
Scope is the whole product here. Every verdict above is true inside the phrase beside it and false outside it. "CONFIRMED at ε = 1/6" is not "CONFIRMED"; "supporting identities only" is not "theorem proved". The claims themselves are stated with more confidence than that at source, which is precisely why an independent scope line is worth having.
This is not a complaint about the authors and it is not a complaint about the AI. It is a measurement of where the checkable surface of a modern mathematical claim actually stops. The exhibits — an eight-atom measure, twenty-four critical points, a quartet of polynomials, thirty decimals of an extremal constant — are all real, and every one of them survived an independent implementation that was trying to break it. The arguments that turn those exhibits into theorems are English prose with mathematical content, and no verifier in this repository or anywhere else can read them.
The one lane where that gap closes is Poisson, and it closes for a structural reason worth naming: a counterexample is an existence claim. Certifying the exhibit IS certifying the claim. Every other lane in this set asks a machine to confirm a universal statement from a finite computation, which it cannot do — so the verdict has to carry a scope line, and it does.
The claim. Five positive point charges in ℝ³ whose potential has at least 24 nondegenerate critical points — exceeding the conjectured bound of 16. Maxwell conjectured that n point charges produce at most (n−1)² critical points of their potential.
Credited system. OpenAI GPT-5.6 Sol (idea); written up by Arathoon, Ball and Kvalheim
Verification at source. Three-author verification; Mathematica and Maple checks — floating point, no code artifact, no certificate, and no concrete ε.
At the fixed rational ε = 1/6 with qε = 859/248832 exactly, 24 pairwise-disjoint boxes, each certifying existence and local uniqueness of a critical point by the Krawczyk operator and nondegeneracy by an interval Hessian determinant that excludes zero. 24 > 16 is then exact integer arithmetic.
The theorem’s asymptotic statement — "for all sufficiently small ε" — and every proof in the paper. One ε is certified, not a range.
The claim. c₂ ≥ 0.4263, via a moment-duality criterion and an explicit rational eight-atom measure (arXiv:2607.17748). The Korenblum constant c₂ had a best published lower bound of 0.3554.
Credited system. OpenAI Codex (GPT-5.6 Sol), disclosed in the paper; author proof by Frank Wikström
Verification at source. An Arb interval certificate shipped with the paper, plus a Zenodo archive.
Every inequality of the paper’s moment-duality criterion for its explicit measure, under our own outward-rounded interval arithmetic — no Arb, no python-flint, and no code from the Zenodo archive executed. The A-family over k = 1..2183, the B-family over k = 1..1299, both tails by exact induction.
The duality argument itself — the paper’s Lemma 3.1 and Wang’s Proposition 2.1. The bound follows from what we certified only if that argument holds.
The claim. The infimum is exactly D = 1.834430475762661711090753635125…, in a July 2026 manuscript of Darvas, Peng and Tao. Among monic polynomials with all roots in [−1,1], what is the infimum of the measure of the set where |f| < 1? Open since Erdős–Herzog–Piranian, 1958.
Credited system. GPT-5.5 Pro (initial main argument in a solver–verifier framework, then revised by the human authors)
Verification at source. Author-checked manuscript shipping its own three Arb certificates and two SymPy verifiers; the official Erdős-problems record was still open.
The extremal triple exists, is unique inside a certified box, lies in the admissible region, and every printed decimal of the extremal constants is correct — including all 30 claimed decimals of D.
The proof that this triple is extremal. We certified the number the manuscript names; we did not certify that no polynomial does better.
The claim. Resolved, in a preprint. Source status: "Human-checked mathematical proof; no formal proof assistant artifact located" (24 Feb 2026). The exact nonreal spectral region for a family of structured matrices — a conjecture in matrix analysis.
Credited system. GPT-5.2 Thinking
Verification at source. Human-checked prose. No artifact of any kind was located.
Every load-bearing polynomial identity of the proof, exactly over ℚ. Both boundary-attainment families re-proved exactly, including an exact re-proof that every nonreal eigenvalue of the A_L family lies ON the conjectured curve. Certified eigenvalue enclosures over 272 exact matrices found zero counterexamples to the necessity conditions, and attainment is Krawczyk-certified at 10 interior points.
The analytic core — the argument parametrization, the convexity/Jensen/Karamata optimization that makes necessity hold for ALL parameters, and the branch bookkeeping. It is prose. This is why the verdict is PARTIAL and not CONFIRMED.
The claim. Exactly the tori — a classification. For which compact connected Lie groups G is the kernel of Haar integration on R(G) a Mathieu–Zhao space?
Credited system. not recorded at source
Verification at source. An author SymPy script, which we read but did not execute.
Every supporting identity the classification rests on, exactly over ℚ with BigInt rational Laurent arithmetic: the weighted witness moments, the explicit abelian pair and its printed four-term expansion, the matrix-entry representatives and their invariance. Disclosure specific to this lane: the author’s Python was READ to cross-check which identities the TeX intended — its blocks match the manuscript and are the ones re-verified here — but it was never executed, and no value on this page came from it.
The classification theorem itself. Confirming the identities a proof uses is not confirming the proof, and this lane is the clearest case of that distinction in the set.
The claim. An explicit counterexample: polynomials R, T, D, S in ℚ[x,q,p,z] with prescribed bracket relations. A conjecture about rank-two Poisson structures.
Credited system. not recorded at source
Verification at source. The author’s own scripts, which we neither derived from nor executed.
All six bracket relations ({D,R} = 1, {S,T} = 1 and the four vanishing ones) hold identically and exactly; the 4×4 symbolic Jacobian determinant is identically 1; and the three claimed points each map exactly to their stated image. A counterexample is an existence claim, so certifying the exhibit IS certifying the claim — the only lane in this set where that is true.
The author’s surrounding prose beyond the extracted definitions. Nothing load-bearing: the counterexample stands or falls on the exhibit, and the exhibit holds.
For Maxwell the move is the whole point: 24 > 16 is exact integer arithmetic once the twenty-four boxes are certified, so at ε = 1/6 the conjectured bound is false, and that much is now independently established rather than asserted from floating-point computer algebra. For Korenblum the move is conditional: our arithmetic puts the criterion beyond doubt and the bound follows only if the paper's duality lemma holds, which we did not audit.
The other four claims do not move a number at all — they settle a question that had no previous numerical answer, or exhibit an object whose existence was open. There is nothing to plot for those, and inventing an axis for them would be the kind of chart this repository does not draw.
The verifiers are plain Node with no packages. Clone the repository and run them; there is nothing to install and nothing to trust from us except the arithmetic, which is the point.
git clone https://github.com/carlostoledo1891/cert-machine cd cert-machine node instruments/laneaudit/audit.js
Each verifier can also be run alone, in its own directory, and prints its own report — the numbers on this page are parsed out of exactly those reports at build time:
node legacy/research/challenges/lane/laneb-maxwell/verify.js node legacy/research/challenges/lane/laneb-korenblum/verify.js node legacy/research/challenges/lane/laneb-lemniscate/verify.js node legacy/research/challenges/lane/laneb-ranteng/verify.js node legacy/research/challenges/lane/laneb-mathieu/verify.js node legacy/research/challenges/lane/laneb-poisson/verify.js
To confirm the verifiers can actually fail, corrupt one and watch it refuse. That is what the 21 mutation controls do automatically on every run: perturb a coefficient, flip a bracket sign, move mass between atoms, replace a candidate with a duplicate. All 21 were rejected in the run that produced this page.
We did not prove any of these theorems and we did not refute any of them. No analytic argument in the set was audited, because none of them is machine-checkable at any budget we have. What we did is narrower: take six results a frontier model helped produce, write independent verifiers from the manuscripts, and report exactly which parts survive exact arithmetic and which parts were never in reach. The verdicts are ours; the theorems remain the authors'. Several of these claims were already checked by their authors, and in two cases by an Arb certificate the authors shipped — an independent reimplementation is worth something anyway, but it is not a first verification and this page never says it is.