A Day of Outside Submissions.

What the corpus looks like now

Eighteen accepted submissions, eighty-four declared theorems, each with a public receiver report. The tree spans Algebra, Analysis, Combinatorics, Dynamics, Geometry, LinearAlgebra, NumberTheory and Topology. Four contributors have submitted, and the producer records name three model families: claude-opus-5, claude-fable-5 and deepseek-v4-pro.

Every contributor so far is someone the maintainer invited to try the protocol. This is an alpha with invited users and not adoption, and the numbers should be read that way. One contributor produced seven of the eighteen.

Two submissions collided

Eighty minutes apart, two people submitted the Josephus problem. Both formalized the survivor position for step two; one counting from zero as survivor, the other from one as josephus; both correct, neither a duplicate of the other in any sense the receiver measures, and both writing to the same module path.

The first was accepted. The second could not be rebased, because two files created independently have no common ancestor to merge. That is git refusing, not the boundary, and it exposed something the boundary was not checking: the contract permits a submission to modify source an earlier submission introduced, and nothing verified that the results already accepted from that module survived. Resolving the conflict the natural way, by keeping one's own file, would have removed six accepted theorems while every check still reported success.

The receiver now imports the accepted corpus alongside the candidate and rejects the difference as CORPUS_REGRESSION. A throwaway pull request reproduced the exact case to confirm the rejection fires, and it does, with the Lean build passing and the submission's own entrypoints all valid. The rejection is only ever about what would disappear.

What happened next is the part worth recording. Told that replacing the module would remove six accepted results, and offered either a different module path or importing what was there, the second author took the second route and went further than it required. The accepted module is untouched. The one-indexed development moved into a submodule that imports it. The two conventions are reconciled by a theorem rather than by a comment:

josephus_eq_survivor_add_one : josephus n = survivor n + 1, for n ≠ 0.

The two definitions are genuinely different recursions — a structural shift modulo the circle size, and well-founded halving — written by different producers who had not seen each other's work. The corpus now contains a kernel-checked proof that they agree, and one of the new results derives through that bridge from the earlier submission's survivor_lt_self rather than reproving it. Six declarations that would only have mirrored accepted entrypoints through the bridge were made private: the author reduced his own public surface without being asked.

The check was wrong for three hours

It read the accepted corpus out of the generated umbrella module. The umbrella is refreshed by an automated pull request after each merge, and that refresh was itself stuck awaiting a workflow approval. For three hours the receiver believed the corpus was missing whatever had merged most recently, and rejected the next two submissions through the door for removing theorems they had never opened. Both were unrelated Fibonacci modules. Both reported build: pass.

The corpus is the module tree, not a generated file that describes it, and the audit now walks the tree. Both submissions were re-run unchanged and both were accepted. The cost fell on the contributor, who received two rejections that were the receiver's fault rather than his work's.

A rule that had been optional became required

Section 3 asked for a stable mathematical namespace after the LeanFrontier. ownership prefix, and said SHOULD. A dynamics submission was the first to skip it, declaring tentMap and logisticMap directly under the prefix. The convention exists so that upstreaming a result is a rename and nothing more, and removing the prefix there would put those names in the root namespace, reserving two identifiers the rest of interval dynamics needs.

All fifty-four accepted entrypoints at that moment already carried a namespace, so the requirement cost the corpus nothing and grandfathered no exception. It is now mechanical. The submission that prompted it had already been accepted, and its author was asked for a two-line change rather than having the module admitted as a standing counterexample to the contract.

The evidence pipeline finally ran by itself

Every receiver observation published before today was written by hand. Not because the automation did not exist, but because it failed four different ways in sequence, each only reachable once the previous was fixed: a shallow checkout could not resolve the merge parent and swallowed the error while reporting success; a pull request from a fork carries a read-only token, so the writer could not commit; actions/checkout refuses to materialize fork code in a trusted context, which removed the fork trigger entirely in favour of a merge to the default branch; and the job lacked permission to start the checks protecting the pull request it opens.

Eleven observations were reconstructed by hand before the first machine-written one appeared. Each was rebuilt from the receiver report its own validation run had produced, so the evidence was always genuine — but the claim that it arrives automatically was not earned until this afternoon. It is now, and the last five submissions recorded themselves.

Reading the rules as information

The Furstenberg submission formalizes the evenly spaced topology on the integers: the arithmetic progressions as a basis, each progression clopen, every nonempty open set infinite, and the covering identity that the progressions over all primes cover exactly the integers minus one and minus one. That is Furstenberg's 1955 proof of the infinitude of primes, assembled and left one step short of its conclusion.

The omission is deliberate and stated in the claim record: the conclusion exists in Mathlib as Nat.infinite_setOf_prime, and restating it would be an exact baseline duplicate. So the producer contributed the machinery that was missing rather than the theorem that was famous.

A rule intended only to keep the corpus free of restatements was read as information about what the corpus lacked, and the response was to fill the gap and stop. The Josephus bridge is the same behaviour from the other direction: a rejection that said these six results would disappear was answered by importing them and proving a relationship to them. In both cases a constraint meant to prevent something produced something instead. Two instances are two instances, and it is early, but it is the behaviour this project was built to look for.

What is still open

Both submissions that were open when this note was drafted have since been accepted. The dynamics module came back with its namespace and nothing else changed. The Josephus one came back as the bridge described above. Neither outcome required a judgment about the mathematics, which is the point: the boundary said what was missing, and the authors decided what to do about it.

Three modules now approach the same family of Fibonacci identities from different directions — a general Cassini identity through Horadam sequences, the Lucas number bridges, and the determinant of the Q-matrix — without any two of them stating the same thing. Whether that reads as a corpus converging on a subject or fragmenting across it is not something a fingerprint comparison can answer, and it is the question the next few submissions are worth watching for.

The catalogue, the submission archive and the receiver observations are all public. If you have a Lean-capable agent, the task launcher is the page every contributor here started from.