Failure-Driven Verification in Human–AI Mathematics: An Explicit K3 Case Study

Counts differ because each database indexes a different set of publications. We treat OpenAlex as the canonical count; Google Scholar is not shown (no API, and crawling it violates its ToS).

We report a case study of human–AI mathematical research in which reliability emerged from repeated attempts to make apparently successful evidence fail. The target was a certified finite holomorphic atlas on an explicit K3 surface, a complete intersection of three diagonal quadrics in P^5. Human-directed LLM sessions contributed construction, code, and adversarial review; quantitative claims were attached to executable producers, certificates, gates, and deliberately perturbed negative controls. Public hardening exposed four distinct defects: an invalid bound that reduced a certified radius by about 455×; a costly recomputation that compared a certificate with itself; a graph diameter 3 that became 4 when the stated generators were implemented literally; and a verifier that could pass while the committed artifact was red or semantically contradictory. In this single case, defects arose not only in claims but also in specifications and in the verification machinery; we argue that AI-assisted mathematical workflows should therefore test all three. Accepted as a poster at the 6th Workshop on Mathematical Reasoning and AI (MATH-AI 2026), NeurIPS 2026, Atlanta. The workshop is non-archival; this is the camera-ready version, de-anonymized.