Verify-in-the-Loop: Proof-Carrying AI Mathematics — a case study certifying, expanding, and stress-testing the Jacobian counterexample with Claude Code (Opus 4.8) and a signing verifier

Abstract

AI now generates mathematics, code, and claims faster than anyone can review them; the limiting resource is no longer generation but trust. The honest response to "I don't trust it" is not "trust me" — it is "here is the check; run it." This deposit is a working demonstration of that response, run on the most scrutinized AI-math result of 2026: the July 2026 counterexample to the 87-year-old Jacobian Conjecture announced by Levent Alpöge with an AI as collaborator. A human directed Claude Code (Opus 4.8) as the proposer, with every mathematical claim compiled and machine-checked by Attestral, a verifier that signs an ed25519 certificate only when its own checker passes. The proposer cannot certify; the adjudicator has no stake in the proposer being right. The output is proof-carrying rather than model-asserted. Working only from the public polynomial list, the loop: independently verified the counterexample (det(JF) ≡ −2 exactly, a rational triple collision); reverse-engineered its mechanism (a non-nilpotent, degree-3 étale endomorphism — outside the classical nilpotent search space); found its hidden cubic (a three-cube-root Cardano fiber) and built an infinite tower of derived counterexamples; mapped the surrounding z-linear construction space (fold-parity obstruction, uniqueness skeleton); proved its natural four-dimensional generalization obstructed at every compensator degree in the Lean kernel; caught three of its own errors mid-run — including a finite-field prime silently collapsing to p = 3 — and discarded them; and reported an honest wall on the nilpotent normal form. Days later the same loop, unchanged, verified the counterexample to the Gaussian Moments Conjecture (Long, arXiv:2607.18186) posted in the same wave. Every claim carries a certificate any reader can re-verify offline: 20 Lean 4 kernel proofs (Mathlib, axiom-audited) for the load-bearing theorems and 23 exact-symbolic certificates (including the Gaussian-Moments companion) for the exploratory identities — two tiers, never blurred. The artifact bundle contains all 43 signed certificates, the Lean sources, the published verification key, and a standalone verifier needing only Python and pynacl: python verify_all.py → 43/43 certificates verified offline, ALL VALID. Scope, stated plainly: we verify and classify; the counterexample is Alpöge's. Certificates settle correctness only; one structural overlap is credited (Shaska, arXiv:2607.20210); no progress is claimed on the still-open plane (ℂ²) case. Interactive companion: https://simgen.dev/attestral/jacobian-counterexample/