From c01317fd624b791de037f8f13fda42cefb9d8a55 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 18:38:50 +0200 Subject: [PATCH] Add field note 13: what trust would skip Co-Authored-By: Claude Opus 5 --- docs/website/notes/field-note-13.html | 76 +++++++++++++++++++++++++++ docs/website/notes/index.html | 6 +++ 2 files changed, 82 insertions(+) create mode 100644 docs/website/notes/field-note-13.html diff --git a/docs/website/notes/field-note-13.html b/docs/website/notes/field-note-13.html new file mode 100644 index 0000000..c53f3ed --- /dev/null +++ b/docs/website/notes/field-note-13.html @@ -0,0 +1,76 @@ + + + + + + + Field Note 13 — LeanFrontier + + + + + +
+ LeanFrontier + +
+
+
+
+

22 September 2026 · Field Note 13

+

What Would Trust Skip?

+

Eighteen submissions landed in one day, seventeen of them from the outside contributor of the last two notes. At that pace, the only step the contributor could not do was the maintainer's merge click, which raised the obvious question: what exactly would it cost to stop clicking?

+
+ +
+

A day at agent speed

+

The corpus went from 33 to 52 modules. Most of the new work formed two clusters. One built out the rational trees: both path enumerations of the positive rationals, the Stern–Brocot interval invariants, and the bridge the contribution directions had marked as high-effort, which proves that a Calkin–Wilf path and a Stern–Brocot path reach the same pair exactly when one is the reverse of the other. The other opened Probability/ with three versions of the Paley–Zygmund inequality, Cantelli's inequality and the Chung–Erdős inequality. Six of the eleven targets in the contributor's own roadmap, which landed in the repository this morning as docs/CONTRIBUTION-DIRECTIONS.md, are now marked as landed there.

+

Every one of them was merged by hand, one at a time. main requires branches to be up to date, so each merge left every other open submission behind; each had to be updated, revalidated for four to eleven minutes, and only then merged, before the next. The mathematics was never the bottleneck.

+
+ +
+

The allowlist question

+

Adding the contributor to the auto-merge allowlist would remove the click, and nothing else. The workflow still waits for the receiver to accept the exact commit, never touches maintenance branches, and hands the merge to GitHub, which still requires every check. So the real question was narrower than it sounded: what does a maintainer's glance at a pull request catch that the receiver does not?

+

The answer is not "a wrong proof". A Lean kernel does not accept one, and the receiver replays every submission through it. It was two things that were not about proofs at all.

+
+ +
+

Two holes that were not about mathematics

+

Code that runs on import. A Lean initialize block runs ordinary code whenever its module is imported. A two-file experiment showed it passing the receiver's list of forbidden constructs untouched, building cleanly, and writing a file on disk the moment another file said import. Anyone depending on LeanFrontier builds it from source and imports it, so that is code execution on their machine. #216 rejects it, along with every other construct that runs at build or import time.

+

Meaning drift. A submission could edit an existing module, and the receiver only checked that every accepted result still existed by name. Redefining something an accepted theorem depends on would keep that theorem compiling while changing what it says. The same pull request made ordinary submissions add-only: extending a module now means importing it from a new one. Of the corpus's accepted submissions, exactly one had ever edited an existing file.

+

Neither hole had been used. Both were there because nobody had asked what a patient contributor could do after a run of good behaviour. With them closed, the contributor stayed off the allowlist anyway: the manual merge is still the cheapest place to catch misleading prose, which no receiver reads.

+
+ +
+

Warnings that become errors

+

The contributor's modules kept using lemmas that the current Mathlib has deprecated. A deprecation is a warning today and an error after the next upgrade, so every one admitted is a future failure of that upgrade's audit. #224 fixed the thirteen already in the corpus, two of them in a module merged an hour earlier, and showed that the whole corpus kept identical statements and axioms before and after. #239 now rejects deprecations in a submission's own files, quoting the replacement Lean suggests.

+
+ +
+

The first conjecture found a bug

+

A conjecture written a month ago and never sent, that the coprimality assumption on the different ideals in Mathlib's compositum discriminant identity cannot be dropped, was finally submitted. The receiver's new probe timings showed six probe attempts where eighteen were due. The conjecture had not been probed at all: an internal list of module names had been overwritten with declaration names, so the receiver found no conjecture to probe in either direction, and had not since conjectures were introduced. #241 fixed it, and the conjecture was admitted with both directions probed. The corpus had held no conjectures before, so nothing had slipped through; the first one to arrive is what exposed the gap.

+
+ +
+

Smaller things

+

The contributor reported that timed-out probes left lean processes running with no parent on their small server, until memory and swap ran out. That was our bug: a timeout killed lake but not the lean it had started. #201 kills the whole process group. And a submission that had fallen behind main was rejected with ten path violations, among them "deleting" another contributor's module, when its only fault was being out of date. #254 reports that case as what it is.

+

Several of these rules changed the receiver during a pre-registered experiment. #240 records them as a dated deviation. The add-only rule in particular creates import edges by construction, and import edges are that experiment's metric.

+
+ +
+

What the day showed

+

A proof checker settles whether a theorem is true. It does not settle what else a file does when it is built, whether a name still means what it meant, or whether a warning will turn into an error. Those are the questions that trusting a contributor would have left unasked. They are now checks, and trusting a contributor is back to being about the prose alone.

+
+
+
+ + + diff --git a/docs/website/notes/index.html b/docs/website/notes/index.html index cfc2c90..4891f90 100644 --- a/docs/website/notes/index.html +++ b/docs/website/notes/index.html @@ -25,6 +25,12 @@

Evidence From the Frontier.

Short records of accepted work, receiver evidence, and the lessons of building a corpus in public.

+
+

22 September 2026 · Field Note 13

+

What Would Trust Skip?

+

Eighteen 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 note +

21 September 2026 · Field Note 12

The Stranger Came Back.