12 September 2026 · Field Note 11
+A Stranger Ran the Same Machine.
+A first-time outside contributor found LeanFrontier, sent a theorem from a fork, and gave the project its cleanest test yet: not whether its maintainer can operate the machinery, but whether an unfamiliar person can reach the same boundary.
+One familiar inequality
+The contribution formalizes Nesbitt’s inequality for positive real numbers: the cyclic sum of a / (b + c) is at least 3 / 2. It clears a positive common denominator and reduces the result to a sum of nonnegative squared differences. The mathematics is classical; this is not a claim of discovery.
What is new to this project is the provenance of the event. The author was not an invited tester, previous contributor, or maintainer. They used the ordinary public submission route and sent exactly one Lean source module with exactly one immutable claim record.
+The only manual action was permission to run
+GitHub pauses workflows from a first-time fork until a maintainer approves them. That is a platform safety boundary, not a LeanFrontier judgement. After approval, the workflow took its receiver code from the trusted base checkout and its candidate only from the fork. The contributor’s workflow never received repository write credentials or the receiver’s authority.
+No one then assessed the proof’s elegance, educational value, or mathematical importance. The restricted receiver ran the same fixed checks as for every ordinary PR.
+The report is the result
+The trusted receiver observation accepted the submission in 107 seconds. It records 61 added lines, no exact Mathlib fingerprint match, a kernel replay pass, a downstream import pass, and an allowed axiom closure of propext, Classical.choice, and Quot.sound.
The one baseline-triviality probe was inconclusive, not self-proving. The receiver also checked the 117 entrypoints already present in the corpus. Those are narrow, mechanical facts. They do not establish that the theorem is useful; they establish precisely what this receiver is built to establish.
+Ordinary afterwards
+After the merge, trusted generators persisted the report, refreshed the catalogue, and synchronised the umbrella module in their own protected changes. The new theorem is now importable as LeanFrontier.Analysis.Nesbitt, with its claim and observation beside it.
That uneventful ending is the point. A corpus only starts to become public infrastructure when a stranger can produce an ordinary contribution whose path is legible, constrained, and the same as everybody else’s.
+