Skip to content

Document the first-time fork submission path #178

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
carlok merged 1 commit into from
Sep 12, 2026
Merged

Document the first-time fork submission path #178

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 60 additions & 0 deletions docs/website/notes/field-note-11.html
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="description" content="LeanFrontier Field Note 11: a first-time outside contributor sent Nesbitt's inequality through the same receiver as every other submission.">
<title>Field Note 11 — LeanFrontier</title>
<link rel="icon" href="../assets/favicon.svg" type="image/svg+xml">
<link rel="stylesheet" href="../assets/site.css">
</head>
<body>
<a class="skip-link" href="#main">Skip to content</a>
<header class="site-header">
<a class="wordmark" href="../" aria-label="LeanFrontier home" translate="no">LeanFrontier</a>
<nav aria-label="Primary navigation">
<a href="../">Project</a>
<a href="../catalogue/">Catalogue</a>
<a href="./">Field Notes</a>
<a class="nav-github" href="https://github.com/carlok/LeanFrontier">View on GitHub <span aria-hidden="true">↗</span></a>
</nav>
</header>
<main id="main">
<article class="note">
<header class="note-header">
<p class="eyebrow">12 September 2026 · Field Note 11</p>
<h1>A Stranger Ran the Same Machine.</h1>
<p class="hero-copy">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.</p>
</header>

<section>
<h2>One familiar inequality</h2>
<p>The contribution formalizes Nesbitt’s inequality for positive real numbers: the cyclic sum of <code>a / (b + c)</code> is at least <code>3 / 2</code>. 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.</p>
<p>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.</p>
</section>

<section>
<h2>The only manual action was permission to run</h2>
<p>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.</p>
<p>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.</p>
</section>

<section>
<h2>The report is the result</h2>
<p>The trusted <a href="https://github.com/carlok/LeanFrontier/blob/main/receiver-observations/nesbitt-inequality/9ea660b09c15b3e3f21a733fbc8f49724805778e.json">receiver observation</a> 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 <code>propext</code>, <code>Classical.choice</code>, and <code>Quot.sound</code>.</p>
<p>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.</p>
</section>

<section>
<h2>Ordinary afterwards</h2>
<p>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 <code>LeanFrontier.Analysis.Nesbitt</code>, with its claim and observation beside it.</p>
<p>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.</p>
</section>
</article>
</main>
<footer>
<p>LeanFrontier is built on <a href="https://leanprover.github.io/">Lean</a> and <a href="https://github.com/leanprover-community/mathlib4">Mathlib</a>.</p>
<a href="https://github.com/carlok/LeanFrontier">github.com/carlok/LeanFrontier <span aria-hidden="true">↗</span></a>
</footer>
</body>
</html>
6 changes: 6 additions & 0 deletions docs/website/notes/index.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,12 @@ <h1>Evidence From the Frontier.</h1>
<p class="hero-copy">Short records of accepted work, receiver evidence, and the lessons of building a corpus in public.</p>
</section>
<section class="section note-list" aria-label="Field Notes">
<article>
<p class="eyebrow">12 September 2026 · Field Note 11</p>
<h2>A Stranger Ran the Same Machine.</h2>
<p>A first-time outside contributor sent Nesbitt’s inequality through the public fork route; the trusted receiver, not a mathematical reviewer, admitted it.</p>
<a class="text-link" href="field-note-11.html">Read the note <span aria-hidden="true">&rarr;</span></a>
</article>
<article>
<p class="eyebrow">31 August 2026 · Field Note 10</p>
<h2>The Fork Was the Test.</h2>
Expand Down
2 changes: 1 addition & 1 deletion tests/test_validate_generated.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ def test_validates_a_regenerated_umbrella_without_executing_lean(self) -> None:
with tempfile.TemporaryDirectory() as temporary:
base = Path(temporary) / "base"
candidate = Path(temporary) / "candidate"
ignored = shutil.ignore_patterns(".git", ".lake", "__pycache__")
ignored = shutil.ignore_patterns(".git", ".lake", ".codegraph", "__pycache__")
shutil.copytree(ROOT, base, ignore=ignored)
umbrella = base / "LeanFrontier.lean"
umbrella.write_text(umbrella.read_text(encoding="utf-8") + "\n", encoding="utf-8")
Expand Down
Loading