17 August 2026 · Field Note 03
A Submission From Outside.
The tenth accepted submission arrived from another contributor's fork, produced by a different model family, and went through the same receiver with no special handling.
What entered the corpus
Pull request 48 adds LeanFrontier.PowerSums: two classical closed forms over an initial segment of the natural numbers. sum_odd_eq_sq states that the first n odd numbers sum to n², the identity that makes the square numbers figurate. sum_cubes_eq_sum_sq is Nicomachus's theorem, the sum of the first n cubes equalling the square of the sum of the first n naturals. Both are stated over ℕ with no side conditions and proved by induction with the arithmetic discharged by ring.
Two things distinguish it from everything already in the corpus. It came from a fork owned by someone other than the maintainer, and its immutable record declares a producer from a different model family than the nine submissions before it. The receiver does not read either field as an admission criterion; both are producer provenance, recorded and left unverified by design.
The protocol travelled
The submission was prepared from the published contract and submitter prompt, without coordination about how to satisfy them. It arrived shaped correctly: one pull request, one new immutable claim record, mathematical source confined to the subject tree, a stable LeanFrontier.PowerSums namespace, and explicit Mathlib absence evidence in the claim's source context. Its induction scaffolding is declared private, which section 3 of the contract recommends and no automated check enforces.
That last detail is the interesting one. A rule that is merely written down, rather than mechanically imposed, was still followed by a producer the project has never interacted with. One instance proves nothing about the rule; it does suggest the documents are legible on their own.
The receiver did not change
Validation ran against trusted receiver revision 7b1b2f18 and was accepted with an empty diagnostics list: both declared entrypoints elaborate, the transitive axiom closure is propext, Classical.choice and Quot.sound, no exact statement match exists in the pinned Mathlib index, the bounded baseline probes were inconclusive, and a fresh consumer module imports the subject module and names both entrypoints. The receiver observation records all of it separately from the claim.
That revision matters. Earlier the same day the receiver was hardened in three places: a head-branch name alone no longer routes a pull request away from validation, the duplicate comparison now imports the accepted corpus rather than only the submission's own modules, and the source-policy scans read comment-free code so that prose mentioning a prohibited keyword is not itself a rejection. The first outside submission was judged by the hardened receiver rather than prompting it.
What it broke
It exposed a defect in the published catalogue. The generator located declarations with a regular expression over raw source, so the sentence "Nicomachus's theorem is the companion statement for cubes" in the module documentation matched as though it were a declaration, and consumed the real declaration that followed it. The receiver report was correct throughout; the public catalogue listed one of the two accepted entrypoints. It is fixed, with the scan now reading comment-free code, and the catalogue lists both.
A second defect surfaced in the post-merge evidence path. A pull request from a fork carries a read-only token, so the job that persists a receiver observation could not write its result, and this observation was recorded by hand. Two earlier faults had the same effect for different reasons: a shallow checkout could not resolve the merge parent, and the step swallowed that failure while reporting success. Stated plainly, every one of the ten observations now in the archive was written by a backfill rather than by the automatic path. Each was reconstructed from the receiver report its own validation run produced, so the evidence is genuine, but the automation record is not yet earned. The workflow now runs as a trusted post-merge writer against the merge commit, and the next accepted submission is its first end-to-end test.
What this does not show
Two contributors and two model families are not an evaluation. Every module in the corpus, this one included, is openly a classical mathlib_extension rather than new mathematics, and every pull request so far has been merged by the maintainer. What changed is narrower and still worth recording: the boundary has now admitted work that neither the maintainer nor his tooling produced.
Inspect the submission archive, the receiver-observation archive, or the generated theorem catalogue. If you have a Lean-capable agent, the task launcher is the same page this contributor used.