The Stranger Came Back.

Extensions, not isolated results

#179 proves the local descent step of the Markov tree: for an ordered positive Markov triple other than (1, 1, 1), the Vieta jump in the largest coordinate is positive, at most the middle coordinate, and so strictly smaller than the largest. It imports the accepted MarkovEquation module and uses its API rather than restating it.

#180 connects the accepted Ford-circle criterion to Mathlib's own geometry: two Ford circles with nonzero denominators are externally tangent, in the sense of EuclideanGeometry.Sphere.IsExtTangent, exactly when their cross determinant squares to one.

Both claims record an agent as the author of the statement and the proof. A human chose the direction from the agent's shortlist, and the claim's source_context says so. The receiver accepted #179 in 111 seconds and #180 in 79. Each had zero exact Mathlib matches, passed the kernel replay and the downstream import, got an inconclusive result from every triviality probe, and passed the check of all 118 and 119 entrypoints already in the corpus. Nothing else about them was assessed.

A question about cadence

The contributor asked whether there was a limit on open pull requests, or anything else that should slow their agent down. There isn't. The practical costs are mechanical: main requires branches to be up to date, so each merge puts every other open PR behind; and a claim pins a Mathlib revision, so an upgrade invalidates open claims until they are bumped. The maintainer added a preference, not a rule: the less trivial, the better.

The contributor also keeps a private map of where the corpus should connect, ranking bridge targets and recording the formulations they rejected, with the reasons. #186 asks whether they'd upstream it.

Their harness found our bug

Before sending anything to the receiver, the contributor's agent runs a plain lake build, because the receiver only ever said BUILD_FAILED. That turned out to be a defect, not a design choice. On a failed build, Lake prints the Lean errors on standard output and only error: build failed on standard error. The receiver kept standard error whenever it wasn't empty, so every build rejection reported just that summary line. #187 keeps both streams, so a rejection now carries the error in the submitter's own file. Admission did not change, only the text of the rejection.

Mathlib v4.34.0, on the third run

The weekly upgrade failed first for a reason outside this repository. Mathlib's download cache had no compiled file for one module, Mathlib.Probability.Kernel.Invariance, so the root Mathlib module was missing too. lake exe cache get reports such gaps as a warning and exits successfully, and the index builder then failed on the missing file. #185 builds whatever the download left out, which took about twenty seconds for those two modules.

The second run built everything, but main moved while it was working, and the upgrade check refused a branch whose evidence predated the new main. That refusal was correct. The third run's evidence was sound, but the independent re-audit ran twice per head under one check name, and the slower copy hit the 45-minute limit twice. #189 gave those jobs more time. #190 now audits each head once, and re-audits it when a maintainer updates the branch rather than silently skipping.

The upgrade landed in #188. The corpus built unchanged on the new release, all 120 entrypoints passed the kernel recheck and the import check, and none turned out to be an exact duplicate of anything new in Mathlib.

What the day showed

An outside contributor working at agent speed stresses the process more than the mathematics. The receiver's verdicts held up every time. What gave way were the edges around it: a message that dropped its evidence, a cache that failed quietly, and a check whose cost nobody had measured on a slow runner. Each is now a test in the repository.