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

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 P5. 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.