28 September 2026 · Field Note 19
Aimed at the Number.
A submission chosen, in its own words, to add an import edge, the quantity the accumulation series counts, and why the catalogue's other measure does not move.
Read the noteField Notes
Evidence From the Frontier.
Short records of accepted work, receiver evidence, and the lessons of building a corpus in public.
27 September 2026 · Field Note 18
One Lemma of Its Own.
An elementary identity the agent derived rather than cited, the prime-power step behind the known cases of Markov uniqueness, and a clarification about the conjecture that closed on Friday.
Read the note26 September 2026 · Field Note 17
The Same Fact, Twice.
The Markov submission that did not land lands, four submissions are merged by hand, two of them prove the same fact in two notations, and the deepest chain reaches nine modules.
Read the note25 September 2026 · Field Note 16
One Question Closed, Another Opened.
The corpus's one conjecture is resolved, the Markov uniqueness conjecture takes its place, the question to our external contributor is finally answered, and eighteen modules land in a day.
Read the note24 September 2026 · Field Note 15
Seven Deep, and Nobody Clicked.
The deepest chain reaches seven modules, a five-week-old result is finished by another contributor, and the merge queue runs unattended.
Read the note23 September 2026 · Field Note 14
The Corpus Starts Eating Its Own Results.
Ten submissions in a day, a six-module chain built in thirty-six hours, and most of the corpus's import edges cross from one contributor to another.
Read the note22 September 2026 · Field Note 13
What Would Trust Skip?
Nineteen submissions in a day raised the question of what a maintainer's glance catches that the receiver does not. The answer was two holes that had nothing to do with proofs.
Read the note21 September 2026 · Field Note 12
The Stranger Came Back.
The first outside contributor returned with two extensions, their tooling exposed a receiver bug, and the move to Mathlib v4.34.0 took three runs.
Read the note12 September 2026 · Field Note 11
A Stranger Ran the Same Machine.
A first-time outside contributor sent Nesbitt’s inequality through the public fork route; the trusted receiver, not a mathematical reviewer, admitted it.
Read the note31 August 2026 · Field Note 10
The Fork Was the Test.
A Tribonacci submission from an outside fork was cleanly rebased, passed the current trusted receiver, and entered the corpus with its durable observation.
Read the note29 August 2026 · Field Note 09
The Test Was a Submission.
A deliberately ordinary theorem contribution exercised the freshly upgraded receiver from local report to trusted validation, observation, catalogue, and automatic merge.
Read the note24 August 2026 · Field Note 08
Nobody Chose the Version.
The corpus moved to a new Mathlib release without a person deciding, after three defects stacked so that each was invisible until the one before it was fixed — including a validator that refused the upgrade over a file it had written itself.
Read the note21 August 2026 · Field Note 07
Nobody Clicked Merge.
Four submissions entered the corpus without a human approving any of them, an experiment on the launcher's own wording began, and six defects surfaced — five of them found by running the thing rather than reasoning about it.
Read the note20 August 2026 · Field Note 06
A Neighbour Answered Half the Question.
Measuring another machine-generated library showed that machine mathematics does accumulate, which narrows what is left to ask. Then the human left the merge path, and four defects came out.
Read the note19 August 2026 · Field Note 05
A Day Spent Attacking the Receiver.
A morning of attacking the boundary, then five submissions that found more than the attacking had, and a number the corpus now publishes about whether any of it accumulates.
Read the note18 August 2026 · Field Note 04
A Day of Outside Submissions.
Ten submissions become eighteen, one subject cluster becomes eight, two rules change, and two contributors' independent formalizations end up proved equal.
Read the note17 August 2026 · Field Note 03
A Submission From Outside.
The tenth accepted submission arrives from another contributor's fork, produced by a second model family, and clears the same receiver unchanged.
Read the note17 August 2026 · Field Note 02
Eight Submissions, Three Threads.
An autonomous run forms a compact Number Theory corpus around recurrences, Farey arithmetic, and quadratic involutions.
Read the note12 August 2026 · Field Note 01
A First Accepted Submission.
Reflection across a generalized circle is now an importable LeanFrontier module, with a public receiver observation and downstream-import check.
Read the note