An AI helped find a counterexample to an 87-year-old conjecture. We rebuilt its entire structure from the public data — and signed every step so anyone can re-check it offline, in seconds, trusting no one.
On 19 July 2026, the mathematician Levent Alpöge announced — with an AI as collaborator — an explicit counterexample to the Jacobian Conjecture, open since 1939. It arrived as a short post. No paper. And the field’s reaction turned on a question it had never had to ask at this speed:
Can we trust a proof no one has had time to check?
That question is the entire subject of this case study. We didn’t find the counterexample — Alpöge did. What we did is arguably more useful in a world where machines now generate mathematics faster than humans can review it: working only from the public list of polynomials, we reconstructed why that counterexample has the shape it does, proved four new structural theorems about the space it lives in, and attached a signed, re-runnable certificate to every single claim. You do not have to believe us. You run the checker.
A famous problem fell in public, in real time. Here is how it unfolded — and where our work fits, one level below everyone else’s.
Alpöge announces a map ℂ³→ℂ³ with constant Jacobian det −2 that sends three distinct points to one output — locally invertible everywhere, yet globally not one-to-one. The Jacobian Conjecture is false for every dimension ≥ 3.
Terence Tao publishes a “digestion.” The Secret Blogging Seminar dissects the fiber geometry. Zihan Zhang catalogs the downstream conjectures that now fall as corollaries. All of it reasons about the map by trusting it.
The popular coverage reframes the event: not “a theorem fell” but “why a tiny social-media post has mathematicians rethinking AI.” The anxiety is specific — can machine-produced mathematics be trusted before review catches up?
From the public polynomials alone, we prove the transport–cone structure, the fold-parity obstruction, the uniqueness skeleton that isolates Alpöge’s map, and the ℂ⁴ frontier — proved obstructed at every degree in the Lean kernel. Every claim signed; all 43 re-verify offline. The answer to the trust question, made runnable.
This isn’t only a mathematics problem. It’s the shape of every field where AI now produces results faster than humans can check them — code, proofs, claims.
A result can be announced in a tweet and consumed by thousands before a single referee has read line one. The bottleneck moved from producing to checking.
Peer review is human time, and human time is fixed. It cannot keep pace with a generator that never sleeps. Reputation is not a proof.
When a model asserts something is correct, there is nothing to independently re-run. You either believe it, or you redo the work by hand.
The counterexample is z-linear: F = A(x,y)·z + B(x,y). Its Jacobian is constant only if three conditions hold — a transport, a compensator, and a scalar closure. Everything below is the anatomy of those conditions. Each card carries the certificate that proves it, re-verifiable offline.
The leading condition det[Aₓ,Aₖ,A]≡0 holds exactly when the surface A traces is a cone. The famous “transport family” is just one cone — provably incomplete.
A homogeneous transport forces the closure to have zero constant term — so it can never be a nonzero constant. A counterexample must carry a degree-0 anchor: exactly Alpöge’s “1”.
The underlying graded fact independently appears in Shaska, arXiv:2607.20210 (Lemma 2.1, Thm 3.2). We claim only the z-linear/necessity reading and cite Shaska for priority. This is the honesty that makes the rest trustworthy.
A z-linear counterexample requires odd fold degree: the closure’s discriminant must be a perfect square, which forces n−1 even. This is why Alpöge’s map is cubic — the smallest odd fold — and why the quartic family collapses.
One weight argument collapses the whole family to a rigid branch and pins Alpöge’s cubic map as isolated, up to scaling, among symmetric z-linear maps. Existence at odd fold ≥ 5 is constrained — and left honestly open.
Four dimensions admit a larger developable transport family that doesn’t exist in ℂ³. We settled its natural candidate: because the anchor is homogeneous, the closure factors as C₄ = x·det[…] — divisible by x for any compensator, so never a nonzero constant. A one-line degree count where a machine search had only sampled — Lean-kernel proven, all degrees. A genuine ℂ⁴ counterexample would need a pole anchor, not a polynomial one.
Supporting the five headline results: z-quadratic backbone, the D₀…D₅ decomposition, canonical-form ⇔ nilpotent (classical, cited), the symbol-map bridge, and the closed-form transport lemmas — 43 certificates in total: 20 Lean-kernel formal proofs and 23 exact-symbolic (including the Gaussian-Moments companion), every one re-verifying VALID, grouped by rung so the two are never conflated.
This is not a figure of speech. Every claim above is an ed25519-signed certificate on disk. One command re-checks the entire structural theory on your machine: it confirms the code hashes match, the signature is valid, and it re-runs the exact checker. The full bundle — certificates, Lean sources, verifier — is permanently archived at Zenodo: DOI 10.5281/zenodo.21567375.
# from the artifact bundle (Zenodo / simgen.dev) — needs Python + pynacl only python verify_all.py # ── output ─────────────────────────────────────────────── FORMALLY VERIFIED — Lean 4 kernel + Mathlib, axiom-audited (20) [PASS] c973a0283a0257f4 Lean alpoge_JH_nonnilpotent [PASS] c6771ba51575fa45 Lean det_one_add_nilpotent [PASS] e8daa77e222d7cb2 Lean cB_C4_never_nonzero_const (ℂ⁴, all degrees) … 17 more kernel proofs … MACHINE-VERIFIED — exact symbolic computation (23) [PASS] 377ceaee812182f4 det(JF) ≡ −2, triple collision [PASS] b8d5376ad450aa97 étale + degree-3 Cardano cube-root fiber … 21 more … ──────────────────────────────────────────────────────── 43/43 certificates re-verified offline (20 formal proofs, 23 machine-verified). ALL VALID — every claim independently re-checked on this machine.
Or interrogate any single claim directly — here, that the map really is a counterexample:
python verify_receipt.py certs/377ceaee812182f4.json 1. code integrity PASS sha256(code) == artifact_sha256 2. receipt intact PASS recomputed receipt_hash matches 3. signature PASS ed25519 over receipt_hash => VALID
Not “an AI says so.” Not “a person vouches.” It means the mathematics was re-checked, from scratch, on your hardware. The signature and the tier answer different questions: the ed25519 signature proves authenticity — this exact code, this verdict, issued under the published key, untouched since — while the tier states strength: formally proved (the Lean kernel accepted the theorem) or machine-verified (an exact symbolic computation passed). Every certificate is both signed and tiered; neither substitutes for the other. The trust is replaced by a computation you control.
Every result here came out of one loop we call Attestral: a verify-in-the-loop engine exposed to Claude Opus 4.8 through a custom Model Context Protocol (MCP) server we built. The model proposes a construction; the checker tries to break it; only when a check passes is an ed25519 certificate signed. The model can propose — it cannot declare. That inversion is what makes the whole classification proof-carrying instead of model-asserted.
The model proposes a lemma or construction in plain, runnable code.
The checker refutes it; the counterexample is fed back; the model revises.
A passing check — and only that — mints a signed, re-verifiable certificate.
The results run at two rungs, and we label every one: the exploratory identities on Attestral’s Python exact-symbolic ladder (23 certificates), and the load-bearing theorems — the nilpotency canonical form, the Alpöge anatomy, the ℂ⁴ obstruction — re-proved in the Lean 4 kernel (20 axiom-audited formal proofs). Machine-checked for the first; formally proved for the second; never one presented as the other. The machine checks, in full:
Attestral spans ten languages and six formal verifiers (Kani, CBMC, Lean, Dafny, F*, TLC). The Lean kernel supplied the 20 formal proofs of the load-bearing theory; the remaining formal rungs weren’t needed for this work, so we don’t claim them.
Three of our own errors were caught and discarded rather than published: a degree-reduction whose own Jacobian check failed, a factor-replacement reconstruction that passed a toy example but failed on Alpöge’s map itself, and — while mapping the ℂ⁴ frontier — a finite-field prime that silently collapsed to 3 yet still printed a plausible “obstructed,” exposed only because we verify the tooling before trusting its verdicts. Catching your own mistakes before they ship is the point.
Look at what everyone else did with Alpöge’s counterexample: Tao hand-verified it, Zhang harvested its corollaries, Shaska classified by weights — all of it reasoning about an object they had to trust. We did something categorically different. From nothing but the public polynomial list — no notes, no search logs, no privileged access — we reconstructed the object’s structural anatomy and attached a proof to every claim.
That matters precisely because of the moment that produced the counterexample. The whole cultural anxiety around it is: “the machine found it — can we trust math that came out of a machine?” Our work is the answer, and the medium is the message:
The counterexample was found by AI, and mathematicians are nervous about trusting it. We used AI to do the opposite of ask for trust — we built a structural theory of that very object where every claim carries a signed certificate anyone can re-verify in seconds, without trusting us or the AI.
That is the shape of the thing worth selling. Not “an AI that does mathematics” — there are many. An independent, mechanical, re-verifiable layer that checks what the machines produce, and leaves behind a receipt anyone can re-run. Demonstrated here on the single most-scrutinized AI-math result in the world.
Correct, new, and important are three different claims. The certificates settle correct. For new, we cross-checked five live sources — and report the one partial collision plainly rather than hide it.
| Source | What it does | Overlap with our structure |
|---|---|---|
| Tao, A digestion | verifies the map (SL₂, resultants) | none |
| Secret Blogging Seminar | fiber geometry, source ≅ 𝔸³ | none |
| Zhang, Direct Consequences | downstream conjecture failures | none — excludes structure |
| Shaska, arXiv:2607.20210 | graded-Keller classification | partial — the anchor (credited) |
| This work | transport, fold-parity, uniqueness, ℂ⁴ | largely unoccupied |
Precise, bounded claims with named limits are the whole credibility of a verifier. Here are ours, stated before anyone has to ask.
The same method that certified this — verify-in-the-loop, signed, independently re-runnable — applies to the code and algorithms your product actually depends on. Numeric, cryptographic, safety-critical, or formal: I’ll assess it and leave you certificates anyone can re-check.
Kyle Clouthier · verifiable & deterministic systems · cryptography, numerical methods, formal verification