三 · 結晶

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.