The Message Was the Fix.

The message was the fix

Field Note 19 left the Varignon perimeter submission rejected: its statement was too large once expanded, and the diagnostic said only that it "exceeds the normalized-term limit". The contributor's agent read "term" as the proof and shrank the proof five times. We rewrote the message the same afternoon. It now says the statement is what is measured, how large it is, what the limit is, and suggests "naming a large subexpression with a definition".

The next attempt, on Tuesday morning, refreshed the claim and stated the perimeter as a named definition: varignonPerimeter a b c d = dist a c + dist b d. It passed. We cannot tell from here whether the agent read the new wording or found the same answer on its own. The submission did exactly what the message says, and nothing it did before the message changed had worked.

It stays the case Note 19 described: the Varignon theorem is used in a proof and mentioned in no statement. By the measure added the same day, it does not count as reuse of the corpus.

A roadmap in three days

On Sunday the contributor replaced the project's roadmap with five new directions. By Wednesday morning each had accepted work. The Furstenberg topology now meets Mathlib's profinite machinery: every finite-index subgroup of the integers is cofinal with the cyclic quotients. Runs of turns in the Stern–Brocot tree were already matched to Euclidean quotients; they now have a canonical one-step interface. The tent map is topologically transitive, and so, through the accepted conjugacy, is the logistic map at parameter four. The eighth cyclotomic field's Galois group is a Klein four group, and its Gaussian subfield joins the square roots of 2 and −2. The fifth direction, Descartes' circle theorem, arrived overnight and is in the next note.

Four of Tuesday's six accepted submissions state their theorems in terms of something already in the corpus, not only in proofs. The corpus ended the day at 102 modules and 80 internal import edges.

Two of our numbers were wrong

The pre-registered series has a column recording whether each submission imports something accepted in the previous seven days. It was computed over every module first seen that day, not over the submission's own modules, so one connected submission marked every other row of its day as connected. Varignon's theorem, which imports nothing, was counted as building on recent work. Corrected, 32 of 96 rows change, all from true to false. The pre-registration records the defect and the fix, and no field note had quoted the measure. The same change adds the measure Note 19 asked for: whether a submission's statements mention something earlier statements mention.

The second was new. The receiver's rejections are now counted weekly, by diagnostic code, without source or submitter. The first published count was wrong the morning it went up: it listed seven weeks of runs in one pass while new runs were being created, the pages shifted under it, and some runs were counted twice and others missed. The week of 17 August showed 44 accepted runs; a count by hand gives 37. The collector now reads one closed week at a time, and the file was rebuilt from scratch.

One check, twenty modules

Monday's Mathlib upgrade had been stopped by the kernel re-check of one module running out of memory. On Tuesday the reason turned up in the checker's own source: asked to check a module, it checks every module whose name begins with that name, all at once. The Markov descent module shares its name with a folder of nineteen others, so checking it meant checking twenty. The module itself costs the kernel 18 milliseconds. Nothing was wrong with it, and the corpus was never at risk: every module was checked, some of them twice. A test now fails before any such family grows past thirty.

Two releases

The corpus has a citable snapshot for the first time: corpus-v1, one record per accepted submission joining its claim, its place in the import graph and the receiver's observation, published with a checksum and the two commands that regenerate it byte for byte. And the library had its first release since 13 August, when it held two modules: v0.2.0, with 102, on Mathlib v4.34.1, tested before tagging by a fresh project that depends on it.