cert-machine · audit · an AI counterexample library
The counterexample machine, decided
Suvrit Sra's open library of counterexamples, most of them 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; four cases rest partly on a cited theorem or an argument over all m, and one holds under only one of the two definitions its own text gives.
The library: github.com/suvrit/count-ex-machina at commit dbf67374 (Apache-2.0), the companion of arXiv 2608.29595, "GPT, the Counterexample Machine". Fourteen cases, mirrored verbatim in corpus/countex. What is decided is each counterexample as the case states it; what the library's authors chose to call a conjecture is theirs. Nothing has been sent to them.
tl;dr
- The finding. 9 of 14 cases CERTIFIED whole; 5 PARTIAL, and no case REFUTED. The partial ones: Borcea-Branden AIM problems (one of four results rests on cited universal theorems); Feasible Picard steps for DPP likelihood (it holds under one of the two definitions of "feasible" its own text gives); Log-volume midpoint gap and its Lorentzian generalization (one of two results needs bodies only a cited theorem supplies); No dimension-free constant in O'Donnell's matrix conjecture (the all-m step is argued in prose); Variance-sensitive Matrix Spencer (the all-m step is argued in prose). The DPP case defines "feasible" twice: as keeping the iterate positive definite, under which a = 5 descends and the conjecture falls, and as Prop. A.1's bound, about 1.90 here, which a = 5 exceeds. None of the fourteen checkers reads the published certificate: each writes it from a witness in its own code.
- The mechanism. One standard-library program per case (4,876 lines in all), written from the case's statement before its verify.py was read, reading the published artifact, recomputing every number the case prints and comparing it as a separate check. Exact rationals and integers; where a transcendental enters, decimal intervals in named contexts with a proved series tail. Each program also decides a FORGE — the certificate changed by the smallest amount that breaks it — which must not certify.
- Check it. python3 tools/run-countex-ledger.py --check · python3 instruments/countex/battery.py — 18 checks, 14 forges refused.
cases decided
14
Found by 16 an OpenAI model, 2 a Claude model, 1 by hand (a case can credit several).
certified whole
9
Every fact the counterexample needs, re-derived from the published artifact.
partly
5
A certified part beside a part that rests on a cited theorem, an argument over all m, or a reading.
checkers that read the certificate
0
Of fourteen. Each writes it; the library's CI checks that the written file equals the committed one.
§1 · the cases
Fourteen counterexamples, one verdict each
| verdict | case | found by |
|---|
| PARTIAL | Borcea-Branden AIM problems | GPT-5 (Pro), GPT-5.6 (Pro), Opus 5 |
| CERTIFIED | Courtade's volume conjecture for Minkowski sums is false | Suvrit Sra, by hand |
| PARTIAL | Feasible Picard steps for DPP likelihood | GPT-5.6 |
| CERTIFIED | Failure of the proposed Hamiltonian NEPv Rayleigh identity | OpenAI Codex |
| PARTIAL | Log-volume midpoint gap and its Lorentzian generalization | GPT-5.6 Pro |
| CERTIFIED | Macdonald lattice Schur-convexity | GPT-5.6 (Pro) |
| PARTIAL | No dimension-free constant in O'Donnell's matrix conjecture | GPT-5.6 Pro |
| CERTIFIED | An oblivious subspace injection need not give relative-error sketch-and-solve | OpenAI Codex |
| CERTIFIED | Exact QRCP can miss the orthonormal-row conditioning bound | OpenAI Codex |
| CERTIFIED | Quantum coupon collection: positivity of an alternating sum of inverses | GPT Pro |
| CERTIFIED | A mixed-norm Cauchy-Schwarz question of Sah, Sawhney, Stoner and Zhao | GPT-5.6 Sol (Pro), Opus 5 |
| CERTIFIED | Strict diagonal dominance does not ensure diminishing Nyström error reductions | OpenAI Codex |
| CERTIFIED | Derivatives of the Jacobi-theta kernel | GPT-5.5 (Pro) |
| PARTIAL | Variance-sensitive Matrix Spencer | GPT-5.5 (Pro) |
§2 · case by case
What is decided, and what the authors' checker does
- Borcea-Branden AIM problems — PARTIAL. Decided: Problems 36, 37 and 38 certified; Problem 35's nonexistence over all positive semidefinite A rests on universal theorems the case cites (Marcus 1963, Lieb 1966, via Wanless 2022) — the witness's own violations of both are certified, the universal step is not re-derived. Found by GPT-5 (Pro) (2026-01-10); GPT-5.6 (Pro) (2026-07-30); bugfixed by Opus 5 (2026-08-10). Their checker: verify_pot.py types in the Kostka matrix and the f^λ values and reads coefficients only at partition exponents, without checking symmetry; nothing is computed for Problem 35 (verify_pencil.py is exact and thorough).
- Courtade's volume conjecture for Minkowski sums is false — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by Suvrit Sra, by hand (2022-05). Their checker: exact.
- Feasible Picard steps for DPP likelihood — PARTIAL. Decided: CERTIFIED when "feasible" means the step keeps the iterate positive definite (the case's context paragraph): a = 5 does, and the likelihood falls. The case's statement block reads "feasibility is the bound a ≤ 1/(1 − γ) of Prop. A.1", and for this L0 that bound is about 1.90, which a = 5 exceeds; under that reading the witness refutes nothing, and the steps tried inside the bound (a = 1, 3/2, 9/5, 1899/1000) all ascend. Found by GPT-5.6 (2026-08). Their checker: exact; never checks the Prop. A.1 bound the statement names.
- Failure of the proposed Hamiltonian NEPv Rayleigh identity — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by OpenAI Codex (2026-08). Their checker: exact.
- Log-volume midpoint gap and its Lorentzian generalization — PARTIAL. Decided: the Lorentzian generalization certified (G strictly Lorentzian, the triangle violation enclosed to 60 digits); the log-volume-distance result needs convex bodies that exist only through a cited realization theorem (Shephard), none exhibited. Found by GPT-5.6 Pro (2026-07-31). Their checker: the arithmetic is exact with a stated series remainder; that G is Lorentzian, and the Shephard inequalities, appear only in prose.
- Macdonald lattice Schur-convexity — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by GPT-5.6 (Pro) (2026-05-14). Their checker: rests on SymPy's simplify (a heuristic, not a decision procedure); positivity for every r is asserted in a comment; the determinant-shift block checks expressions typed in by hand.
- No dimension-free constant in O'Donnell's matrix conjecture — PARTIAL. Decided: every family member to m = 11 certified (unit trace, PSD, ratio above m/32; built exactly, densely at n = 512); unboundedness over all m, which refuting a universal constant needs, is argued in prose (a trace-norm duality bound and dyadic sums past m = 14). Found by GPT-5.6 Pro (2026-08). Their checker: never builds R: the diagonal is assigned (diagonal = list(eigenvalues); diagonal[0] -= delta; diagonal[-1] += delta), the induction is written in rather than run, and the dyadic bounds are not checked.
- An oblivious subspace injection need not give relative-error sketch-and-solve — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by OpenAI Codex (2026-08). Their checker: the residual formula and OPT = 1 are typed in (residual_squared = x_tilde * x_tilde + F(1)).
- Exact QRCP can miss the orthonormal-row conditioning bound — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by OpenAI Codex (2026-08). Their checker: exact; relies on the prose step Q(I,:) = H^(-1/2) and does not check P_II^(-1) = H.
- Quantum coupon collection: positivity of an alternating sum of inverses — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by GPT Pro (2026-02-16). Their checker: exact; writes "proved_positive_definite_for_n": [1, 2, 3, 4, 5] into the certificate without a check.
- A mixed-norm Cauchy-Schwarz question of Sah, Sawhney, Stoner and Zhao — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by GPT-5.6 Sol (Pro) (2026-07-13); Opus 5 (2026-08). Their checker: the general result rests on SymPy's deficit.is_negative is True, which settles the sign of such a number by evaluating it (sound here, the deficit is about −5.15); the B = A result is an mpmath point value, assert ratio > mp.mpf("1.0000006"), the interval certificate living in a Sage script verify.py does not run.
- Strict diagonal dominance does not ensure diminishing Nyström error reductions — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by OpenAI Codex (2026-08). Their checker: exact; positive semidefiniteness is checked on the complement block only.
- Derivatives of the Jacobi-theta kernel — CERTIFIED. Decided: every fact the counterexample needs, re-derived from the published artifact. Found by GPT-5.5 (Pro) (2026-02-22). Their checker: no tail bound ("m>=20 is astronomically negligible; see Sage certificate for rigorous tail"), a point comparison; the rigorous part is a Sage script verify.py does not run.
- Variance-sensitive Matrix Spencer — PARTIAL. Decided: m = 2..10 certified exactly (discrepancy by exhaustion, ratio squared up to 81/11 at m = 10); unboundedness over all m, which refuting a universal constant needs, is a three-line argument in the case's prose, checked by hand and not by code. Found by GPT-5.5 (Pro) (2026-05-24). Their checker: exact, for m in (2, 3, 4) with three U each; "unbounded in m" appears only as a string in the certificate.
§3 · one case, two definitions
When is a step feasible?
The DPP case refutes a conjecture of Mariet and Sra (2015): that every feasible Picard step a ≥ 1 increases the log-likelihood. Its context paragraph says a step "is feasible when it keeps the iterate positive definite, which the source guarantees for a ≤ 1/(1 − γ)"; its statement block says "feasibility is the bound a ≤ 1/(1 − γ) of Prop. A.1". The witness takes a = 5.
- Under the first reading it holds. L₀ and L₁ = L₀ + 5·L₀ΔL₀ are both positive definite, and the log-likelihood falls: decided exactly, every printed number reproduced.
- Under the second it refutes nothing. For this L₀ the bound 1/(1 − γ) is about 1.90, and a = 5 is outside it. The steps tried inside the bound — a = 1, 3/2, 9/5 and 1899/1000 — all ascend.
The source's own sentence, "Prop. A.1 presents an easily computable upper bound on feasible a", reads more naturally the first way, so the counterexample stands for the conjecture as posed. What it does not show is a descending step that Prop. A.1's bound admits; that question is still open, and the case's statement block, as written, asks it.
§4 · the checkers
What a checker that writes its certificate proves
Every case's verify.py builds its witness from values in its own source and WRITES artifacts/ from them; none of the fourteen reads the published certificate. The library's CI then regenerates the artifacts and requires git diff --exit-code, so the committed files equal what the code writes — but a reader holding only a certificate cannot check it with verify.py. The deciders here read the published artifacts.
That design makes each certificate reproducible, which is worth having. It does not let anyone check a certificate they were handed, and several checkers type in what they should compute: a diagonal assigned rather than built, a residual formula written in, a Kostka matrix copied, a sign settled by SymPy's numerical evaluation, two tails left to Sage scripts the Python checker does not run. In every case the mathematics survives the stricter decision here; the point is where the rigor sits.
§5 · limits
What is not decided here
- Universal theorems a case cites. Marcus 1963 and Lieb 1966 for the AIM Problem 35; Shephard's realization theorem for the log-volume distance. Their conclusions are used, not re-derived.
- Arguments over all m. Refuting a universal constant needs a family that is unbounded; the finite members are certified (to m = 11 and m = 10) and the step to all m is prose, checked by hand here and not by code.
- The deciders' origin. They were written in this session by three parallel agents, each from the statements before reading the authors' checkers, and are published with the ledger; they are checked by their forges and by agreement with every printed number, not by a second independent implementation.