The Receiver Misread It.

Into Mathlib's continued fractions

Sunday's submissions proved that the runs of a Stern–Brocot path are the quotients of Euclid's algorithm on the fraction the path reaches. Tuesday's takes the last step: Mathlib's own computation of a continued fraction, applied to that fraction, returns exactly those quotients. One adjustment is needed. A fraction below one has a regular continued fraction that starts with zero, which the corpus's quotient list leaves out, so the submission puts it back exactly when the path starts with a left move.

It is the first module to use Mathlib's continued fractions. It imports the quotient sequence and mentions it in its statements, so both measures count it as building on the corpus. It does not use the run-length encoding that landed with the quotient sequence. Field Note 22 noted that the two define the same recursion. Two days later, nothing imports the encoding.

The corpus stands at 108 modules and 87 internal import edges.

Half a statement

Before checking a theorem, the receiver reads its statement out of the source: where the claim ends and the proof begins. On Sunday we found it had been missing every theorem proved by cases, where the proof is a list of lines starting with a bar and there is no :=. It had never probed four accepted theorems for triviality. We taught it to stop at the first such line.

Tuesday's submission states one of its theorems with a case split inside the statement. The receiver stopped at the first bar of that split and read the claim as ending in match path with. A probe on half a statement cannot run, so it was recorded as inconclusive, and the submission's own report said the same. The submission is sound: the build, the kernel recheck and the statement fingerprint do not depend on this reading. But "inconclusive" meant "not tried".

The repair follows Lean's own rule. Bars right after with belong to the case split, and so do all the bars after them. A named argument such as (n := 3) no longer ends a statement either. Over the corpus's 548 statements, one reading changes: this one.

Neither bug showed up in the receiver's own tests. The first turned up because the catalogue was missing two theorems. The second turned up while reading a submission to write about it.

The first scheduled week

On Monday the rejection collector ran on its own for the first time and added one week, from 28 September: 22 accepted validation runs, 5 over a resource limit, 2 that did not build and 1 with a malformed claim. These count runs, not submissions; a submission revalidated after its branch is updated counts again. The file now covers seven weeks.