A Day Spent Attacking the Receiver.

The morning did not move the corpus

It opened at eighteen accepted submissions and eighty-four theorems, where it had closed the night before. The next five sections are about the receiver rather than the mathematics, which is the less photogenic half of the experiment and the half that decides whether the other half means anything. The corpus did move later, and the last two sections are about what happened when it did.

A family could be smuggled in two pieces

The receiver rejects a repeated literal or permutation family: three declarations sharing one normalized skeleton fail as DEGENERATE_THEOREM_FAMILY. It counted only within a single submission. So two members could arrive today, scoring two against a threshold of three and passing, and the rest could arrive tomorrow against a counter that had reset.

Exact-duplicate detection did not cover the gap, because members of such a family differ by construction — that is what makes them a family rather than a duplicate. The check now counts candidate skeletons against the whole accepted corpus, and the threshold comes from the versioned policy file rather than a number hardcoded beside it.

A throwaway pull request confirmed it fires on the real receiver: two numeral variants of an accepted statement, rejected as three declarations share one literal-normalized skeleton, one of them already accepted. Before the change those two would have scored two, and been admitted.

The policy files advertised six switches that did nothing

The boundary is supposed to be readable from policy/. Comparing those files against the validator found six keys nothing read: a family threshold that the code hardcoded beside it, an identifier length limit enforced nowhere, and four describing behaviour that was fixed rather than configurable.

Each was wired up or removed. Two survivors, the memory and disk limits, are genuinely enforced — by the container the validator runs inside rather than by the validator itself — and a test now asserts the workflow's flags match the numbers the policy claims, so the two cannot drift apart. A further test walks both files and fails if any key is unread, which is the only way this stays true.

Reading a neighbour

LeanFrontier is not the only Lean library downstream of Mathlib built for machine-generated work. Tau Ceti keeps mathematical judgment and moves it, with human-written roadmaps directing what may be added and AI reviewers scoring submissions against rubrics. merely-true removes review and anchors trust in contributor identity instead.

Reading the second one surfaced a real gap here. It runs leanchecker, which replays compiled declarations against the kernel. LeanFrontier did not: the axiom closure came from collectAxioms over the environment the build produced, so admission rested on the elaborator's word for a project whose entire claim is that the kernel decides. That was closed the same day, extended to the release-upgrade audit, and every module in the corpus was rechecked by hand at the current pin. All nineteen pass. The gap was real and merely-true was right about it.

The local command disagreed with the authority it predicts

Submitters are told to run the receiver before opening a pull request. In a working tree it reported path policy violations on .DS_Store and on the coverage file the documented test command writes — findings CI never produces, because it validates a clean checkout. So the rehearsal failed where the performance would have passed, on every macOS machine, at first contact.

The ignore set now derives from the repository's own .gitignore, read from the trusted tree rather than the candidate: a submission able to widen that set could hide files from the receiver.

The evidence pipeline stopped needing a human

Field Note 04 recorded that the post-merge writer finally ran unattended. It did, but every pull request it opened then waited for a person, because a pull request opened with the default token does not trigger the checks a ruleset requires of it. Yesterday that meant twenty-three generated pull requests, each needing a manual approval, and four consolidations written by hand.

The generators now authenticate as an application installation. A deliberate probe made the umbrella stale, the generator noticed, opened a pull request as itself, its checks started without anyone asking, and it merged and restored the file. Nothing in that sequence required a human after the trigger, and the count of runs waiting for approval was zero.

Then the submissions arrived

Three landed in the afternoon. The greatest sequence with bounded increments below a partial ceiling, reached from a doctoral thesis on two wheeled vehicle dynamics, where the forward and backward passes of a lap time simulator compute exactly that object; the module states it in order theoretic terms and nothing physical enters the Lean. Then a small extension of it. Then Stedman's plain changes from 1677, the sequence of rows in which consecutive rows differ by one adjacent swap, whose step invariant is a constructive Hamiltonian path in the Cayley graph of the symmetric group under adjacent transpositions, rediscovered three centuries later as the Steinhaus-Johnson-Trotter enumeration. That one filled the group theory directory, empty since the bootstrap, and reused Mathlib's permutation machinery rather than restating it.

Two more followed in the evening, both from a fourth model family, and they are the subject of the two sections after next. The corpus closed at twenty three submissions, ninety nine theorems, ten subject areas.

What real submissions found that attacking had not

Merging the first of them opened three generated pull requests at once. The umbrella one merged, which moved the default branch, which left the other two behind with every check green and no way to proceed: the ruleset requires a branch to be up to date and automatic merging does not update branches. Both needed a manual command.

Worse, one of the two should never have existed. The catalogue renders three inputs, and a submission merge changes two of them in a single push while the third, the receiver observation, does not exist yet. So the catalogue sync produced a render with no receiver report links at the same moment the observation writer produced the complete one. Had it merged it would have stripped eight links from published output. It was closed instead, and the sync now defers to the observation writer whenever a submission record changed in the push it is reacting to.

The stranding was fixed the other way round, by having every merge bring forward whatever it stranded. Both fixes were then confirmed by the two submissions that followed rather than by a probe: two generated pull requests per merge instead of three, and the straggler carried forward without anyone touching it, twice.

Neither failure was reachable by attacking the receiver directly. Maintenance pull requests take a different path and produce no generated output at all, so a week of them would not have surfaced either one. That is the argument for the corpus being the thing that tests the machinery, and against believing a boundary is sound because its author cannot break it.

A word the contract had never defined

Every submission declares who authored its statements and its proofs. Twenty one records in, twenty read machine and one reads mixed, and the outlier is the first submission ever accepted. Several of the twenty describe, in their own context field, a human who named an area or chose from a shortlist the producer proposed.

The contract required the fields and the schema listed their values, and nothing said what they measured. It now does: they ask who wrote the formal text, not who chose the subject, so a human posing a vague direction leaves the answer machine and the human's part belongs in the context field. The older record stands as it is. Records are immutable, and a contract that explains an inconsistency is worth more than a history quietly edited to remove one.

A theorem that cannot be used yet

The exponential form of Hermite-Lindemann says that the exponential of a nonzero algebraic number is transcendental. The pinned Mathlib release does not export it; an upstream pull request is in flight and was inspected at a named commit to confirm it does not contain the corollary below. So the submission takes the theorem as an explicit premise and derives, in six lines, that complex exponentiation is injective on the algebraic numbers: if two algebraic numbers have equal exponentials, their difference is algebraic and nonzero, so its exponential is transcendental, and that exponential is one.

This is the corpus's first conditional theorem, and it will become directly instantiable the day the premise reaches a release. It also opens a category the boundary does not measure. A conditional statement is only as meaningful as its hypothesis is satisfiable, and nothing here checks that. A theorem assuming zero equals one would build, contain no incomplete proof, depend on no forbidden axiom, duplicate nothing, and resist every bounded probe, while saying nothing at all. This submission is on the right side of that line and the receiver cannot tell why.

A theorem stronger than the one upstream

The last submission of the day was the first to use the autonomous discovery mode, which had existed in the contract unused since the beginning. The human asked for the process without naming a subject. The producer generated three candidates from the pinned tree, the product of all elements of a finite commutative group, the vanishing sum of a nontrivial character, and the parity of the non-fixed points of an involution, and chose the second for its generality and short structural proof.

Mathlib already has that theorem, for a commutative integral domain. This one drops commutativity from the codomain and asks only that the ring have no zero divisors, so the upstream statement is a special case of what now sits in the corpus. The proof is also shorter than the one upstream, which establishes cyclicity of the image in the unit group first; this one reindexes the sum by left multiplication and factors, and commutativity never appears because it was never needed.

That is the most valuable shape a corpus like this can produce, and it exposes the mirror of the previous section's problem. Weakening a hypothesis changes the elaborated statement, so the duplicate check sees something new, correctly. Strengthening one changes it too. A submission that took an existing Mathlib theorem and added an unnecessary assumption would be strictly weaker than what already exists, structurally indistinguishable to the receiver, and pure noise. Generalisation and its opposite look identical from here.

The number the corpus now publishes about itself

Novelty is easy to mistake for value here. Eighty-eight of the ninety-nine accepted statements mention a definition that exists only in this corpus, so no literature can contain them word for word. That sounds like a strong result and is mostly self-reference: a submission proving things about the definition it has just introduced. It rules out one failure, verbatim restatement, and says nothing about the one that matters, which is whether any of this accumulates.

The question is about the dependency graph, so the graph is now measured and drawn in the catalogue, regenerated on every merge. Twenty four modules, four internal import edges, which is 0.17 edges per accepted submission. Twenty six corpus constants appear in some statement and four of them appear in statements from more than one submission. The picture that goes with those numbers shows four small clusters and sixteen modules standing alone.

Two measures rather than one, because they are not equally honest. An import costs a single line and need not be used, so anyone optimising for a published ratio can raise it for free and the receiver would not notice. A corpus constant reaching another submission's statement means a theorem was written about it, and that cannot be faked without writing the theorem. The catalogue says which is which, on the page, so the first contributor who reads the ratio and considers improving it reads the caveat in the same breath.

A metric published only when it flatters is not evidence, which is the argument for wiring it into the generated output rather than into a note. If the ratio climbs, machine mathematics is depending on machine mathematics and the premise has something behind it. If it stays near one edge per six submissions, what exists is a growing collection of correct and independent libraries. That is a fine thing to have built and a different claim from the one on the front page.

What this was

Twenty merged changes. The morning's came from one question asked repeatedly, about what a producer wanting volume rather than content could get away with, and from reading somebody else's project carefully enough to find they were right about something. Everything after came from people using the thing, and found more.

One of the five submissions was produced by the same assistant that wrote most of the receiver, and says so in its record, because a project whose premise is declared provenance should not have to be asked about that. It is a small result about a definition an hour old. Whether it belongs in a corpus of machine generated mathematics is a fair question, and the disclosure exists to make it answerable rather than to settle it.

The day ends with three open questions that no check answers, and the first is now at least counted rather than assumed. Whether the corpus accumulates is a number on the catalogue, and today that number is low. The other two are: whether a conditional theorem's hypothesis can be satisfied, and whether a statement that differs from a known one is stronger or weaker than it. Both were found by submissions rather than by review, both are about meaning rather than validity, and neither is obviously mechanisable. Recording that a submission is conditional, or that it stands in a strengthening relation to something known, would at least make the categories visible without asking the boundary to judge them. That is the next thing to try.