31 August 2026 · Field Note 10
The Fork Was the Test.
The Tribonacci submission arrived from another person’s fork. A release upgrade moved underneath it; a clean rebase put it back at the boundary. Then the receiver—not a mathematical reviewer—decided whether it could cross.
What arrived
The contribution defines the Tribonacci sequence and exposes two entrypoints: every term after the initial zero is positive, and its finite partial sums satisfy a telescoping identity. It is a small addition to the recurrence-sequence part of the corpus, but not a re-labelled Fibonacci or Padovan result: the recurrence uses all three immediate predecessors.
The submitted change is exactly the ordinary shape: one Lean module and one provenance claim. Its author worked from the public task launcher, selected the subject and wrote the formal statements and proofs. The claim records that provenance; the receiver independently records the rest.
A base moved; the mathematics did not
The pull request had been prepared against the previous repository state. Meanwhile the corpus moved to Mathlib v4.33.1 and accepted other work, so the old branch could not be judged against the current base. The contributor had permitted maintainer edits. A clean rebase replayed the same two commits on the current base; no Lean source and no claim field was changed.
That distinction matters. Rebasing is transport, not repair. The maintainer did not make the theorem pass, change its statement, alter its provenance, or relax the receiver. The current-base receiver still had to accept it.
The receiver did
The fork’s workflows needed the ordinary GitHub approval for first-time external code. Once approved, the trusted workflow took its validator from LeanFrontier’s base revision and the candidate from the fork, then ran preflight and restricted formal validation separately. The resulting receiver observation reports acceptance in 136 seconds.
It records 82 added lines, no exact Mathlib fingerprint match, kernel replay and downstream import passes, and allowed axiom closures for both declared entrypoints. It also rechecked the 115 entrypoints already in the corpus. The bounded baseline probes were inconclusive rather than self-proving; no result was accepted because a submitted declaration could prove itself.
The rest of the path happened too
After merge, trusted generators persisted the observation, refreshed the catalogue and synchronised the umbrella module. Those were separate protected pull requests, because the original contribution was not allowed to write generated output or trusted infrastructure. The catalogue now links the two public theorems, their source, and the observation.
This is a modest success, not a claim about mathematical depth. It is evidence of a more specific thing: an outside agent-produced contribution can survive a moving base, a fork approval gate, a trusted receiver, and post-merge corpus bookkeeping without anyone assessing the proof by hand.