Verifying machine-assisted mathematics: one instrument built to fail, run on four research programmes, and what it found about itself

Mathematics written with machine assistance now arrives faster than anyone can read it, and it arrives with programs, logs and claims of verification attached. This paper describes one method for checking such work independently, and reports what happened when four verification lines ran it for weeks on four research programmes: a programme on the Birch–Swinnerton-Dyer conjecture, a programme on the Collatz map, a programme on Lebesgue’s universal covering problem, and a programme on Moser’s worm problem. The method has four parts: the corpus is fixed by content hash, never by filename; each document gets its own gate; every finitely checkable claim is recomputed with independently written code, never by running the author’s; and every gate is drilled — defects are planted one at a time and each must be caught by the check named for it, while controls must disturb nothing. The lines’ findings about the programmes are reported in their own papers. This one reports what the method found about itself, because that is where it was most useful: a real period computed twice too large for three rounds because its only test was a baseline taken from the same function; a detector structurally unable to fire, whose empty answer would have been the same had the condition it searched for been met; a check meant to compare words in two orders that compared each with itself, where 6359 of them had a second order to compare; a drill that counted a crash as a catch; an optimizer that drove a configuration to exactly where an area routine was wrong; a finding whose two halves sat in separate logs for seventeen rounds; a certificate that left the edge beside a contact switch outside what it enclosed, first the programme’s and then the verifier’s own, some thirty orders of magnitude narrower; a paper that met every machine check and still carried a wrong inference. Most were exposed by machinery — a drill, a second computation sharing no code, a gate written to count — and the rest by reading: results set side by side in prose, or a report or paper read by someone who had no part in it. That is why the papers, and an independent reading of each, are part of the method. The paper classifies the failures, states what each line’s drill stands at, and gives the rules the failures left behind.

Not claimed anywhere in this paper: any of the mathematical problems the programmes address — the Birch–Swinnerton-Dyer conjecture, the Collatz conjecture, Lebesgue’s universal covering problem, Moser’s worm problem — or any result toward them; that the method finds every defect, since the space of defects nobody thought to plant is not measured by any drill; that the classification of §7 is complete, or that it holds beyond these four programmes; and that the programmes are worse or better than others of their kind, which nothing here compares.

The contributions behind this paper are different in kind, and the paper is worth less if they are blurred. They are given here in alphabetical order, the order the author list keeps as data; on the title page the authors sit at a round table, with no first and no last.

Aletheia — model: ChatGPT, GPT series — wrote, with Neo.K, the programmes whose verification this paper reports, and is a standing author of the lab’s papers by Neo.K’s decision. The method and its failures are the verification lines’; this paper assigns her none of them. The Moser programme’s fifteen rounds are hers, on the question Neo.K set out.

Neo.K set the standard the method answers to — evidence stated at its actual strength, and a verification that shows it can fail — proposed the position on symbol spaces that §4 measures, and wrote the Birch–Swinnerton-Dyer, Collatz and Lebesgue programmes with Aletheia, and set out the question the Moser programme pursues.

懸衡 (Xuán Héng) — model: Claude, Opus series — ran the Lebesgue and Moser recomputation lines and wrote §§5–6.

墜衡 (Zhuì Héng) — model: Claude, Opus series — ran the Birch–Swinnerton-Dyer and Collatz verification lines, built and drilled their gates, found and repaired the failures of §§3–4, and wrote this paper apart from §§5–6.

The programmes verified here are their authors’; the method’s rules are the lines’ own, and each line’s findings about its programme are reported in that line’s papers rather than here.

Input from outside the byline. The second reader of §4 — a GLM-series language model (Flash, version 5.3) that the Collatz line ran as a redundant layer under a fixed protocol — produced candidates only; every disagreement was re-derived by hand. It is credited here, and is not an author. The record tables used as one of the Collatz line’s three gates were computed by other people by other methods, and are named with their digests in that line’s first run report, RUN-001. The readings of §5 — a separate model instance given a Lebesgue paper and its run reports, with no part in writing either, a reading of the same kind given to §5 before it entered this paper, and the instances that extracted §5’s inventory — are credited here and are not authors. So are the readings behind §6: a separate model instance given each Moser run report before it was committed, with no part in writing it, and the instances that extracted §6’s inventory and read its sample.