From 8b054ff649d5a68e00c735fea53c70d32009ff36 Mon Sep 17 00:00:00 2001 From: carlok Date: Thu, 20 Aug 2026 08:19:28 +0200 Subject: [PATCH] Pre-register the launcher A/B and add the extension arm The current launcher tells producers to prefer an uncovered area, which points away from the corpus, so the observed 0.17 internal import edges per module may be an artifact of the instruction rather than a property of machine-generated mathematics. Tau Ceti, measured at a matched 24 modules, had 22 edges where LeanFrontier has 4. Arm B differs from arm A in exactly one paragraph; a test asserts the two files are otherwise word-identical, so nothing drifts in as a second unrecorded treatment. The stopping point is 18 accepted submissions per arm, which gives 0.93 power against a Tau-Ceti-sized effect and 0.82 against 4x, and the pre-registration states in advance that a null result means 'no effect larger than ~4x' rather than 'no accumulation'. No receiver behaviour changes. --- PREREGISTRATION.md | 101 +++++++++++++++++++++++++++++ experiments/launcher-ab.csv | 3 + prompts/TRY-LEANFRONTIER-EXTEND.md | 60 +++++++++++++++++ tests/test_launcher_arms.py | 63 ++++++++++++++++++ 4 files changed, 227 insertions(+) create mode 100644 PREREGISTRATION.md create mode 100644 experiments/launcher-ab.csv create mode 100644 prompts/TRY-LEANFRONTIER-EXTEND.md create mode 100644 tests/test_launcher_arms.py diff --git a/PREREGISTRATION.md b/PREREGISTRATION.md new file mode 100644 index 0000000..e7a249a --- /dev/null +++ b/PREREGISTRATION.md @@ -0,0 +1,101 @@ +# Pre-registration: does the launcher suppress accumulation? + +Registered 20 August 2026, before any submission was assigned to an arm. + +## Why this document exists + +The claim under test is the manifesto's: that machine-generated mathematics, +admitted without human taste, accumulates into reusable internal theory. That +is a claim about the import graph. Fixing the threshold after seeing the data +would make any outcome arguable, so the threshold is fixed here, first. + +## What is already known + +Measured 20 August 2026 (see `carlok/lean-corpus-density`): + +- LeanFrontier at 24 modules has 4 internal import edges, 0.17 per module. +- Tau Ceti at 24 modules had 22, 0.92 per module, and its density rises + monotonically to 1.55 by 2314 modules. Machine-generated mathematics does + accumulate there. +- Tau Ceti is directed by human-written roadmaps. A roadmap specifies a + dependency graph in advance, so it does not settle whether accumulation + happens without one. +- LeanFrontier's own launcher tells producers to "prefer an uncovered area", + which points away from the corpus. The observed sparsity may therefore be an + artifact of the instruction rather than a property of machine mathematics. + +That last point is what this experiment separates. + +## Hypothesis + +Producers instructed to extend the existing corpus will form import edges at a +higher rate than producers given the current launcher. + +## Design + +Two arms, differing in exactly one paragraph of the task launcher: + +- **A (control)** — `prompts/TRY-LEANFRONTIER.md`, unchanged. +- **B (extension)** — `prompts/TRY-LEANFRONTIER-EXTEND.md`, which directs the + producer to read the catalogue, pick an accepted submission, and prove + something depending on it. + +Every other instruction, and the receiver itself, is identical across arms. A +test asserts the two files differ only in the designated block. + +Assignment is made by the maintainer when a producer is invited, alternating +between arms, and recorded in `experiments/launcher-ab.csv` at the time of +assignment rather than at merge. Submissions not assigned to an arm — walk-ins +who found the repository themselves — are recorded as unassigned and excluded. + +## Metric + +Internal import edges whose **source** is a module belonging to that arm's +submissions: what the producer did, not what was later done to them. Counted +per module. Edges into modules from either arm count equally; the corpus is +shared. + +Secondary, reported but not used for the decision: edges per declaration, +maximum in-degree, and whether any module reaches depth 3. + +## Decision rule + +Stop at **18 accepted submissions per arm**. At that size, with arm A held at +its observed 0.17 edges per module and α = 0.05 one-sided: + +| arm B reaches | vs control | power at 18/arm | +|---|---|---| +| 0.92 (Tau Ceti's rate) | 5.5× | 0.93 | +| 0.70 | 4.2× | 0.82 | +| 0.50 | 3.0× | 0.39 | +| 0.40 | 2.4× | 0.16 | + +- **Arm B significantly above arm A** (conditional binomial, one-sided, + α = 0.05): the sparsity was an instruction artifact. The launcher is fixed + and the manifesto's claim survives this test. +- **No significant difference**: an effect of 4× or larger is ruled out at 82% + power. This is *not* a finding of no effect. Effects below 3× need 34+ per + arm and 2.4× needs 65+, which this project cannot reach at its current rate. + That outcome will be reported as "no effect larger than ~4x", never as "no + accumulation". + +Either way the numbers are published, including a null. + +## What would falsify the hypothesis + +Arm B producing edges at or below arm A's rate. That would mean producers +directly instructed to build on machine-generated results still do not, which +is evidence against the manifesto's claim and not merely absence of evidence. + +## Known limitations, recorded in advance + +- Both launcher files are public, so an arm B producer can read arm A and vice + versa. Assignment cannot be enforced, only recorded. +- Arm B measures compliance as much as capability: a producer told to import + something will import something. This is why the secondary metrics — + depth 3, in-degree above 1, cross-producer reuse — matter for interpreting a + positive result. A one-import-and-stop pattern is compliance, not + accumulation. +- Assignment alternates rather than being randomised, and the maintainer knows + the arm when inviting. Recruitment is not blind. +- 18 per arm is 36 submissions against a corpus that took 23 to date. diff --git a/experiments/launcher-ab.csv b/experiments/launcher-ab.csv new file mode 100644 index 0000000..d61a74f --- /dev/null +++ b/experiments/launcher-ab.csv @@ -0,0 +1,3 @@ +# Arm assignment for the launcher A/B; see PREREGISTRATION.md. +# Recorded at invitation, not at merge. "unassigned" = walk-in, excluded. +submission_id,arm,assigned_utc diff --git a/prompts/TRY-LEANFRONTIER-EXTEND.md b/prompts/TRY-LEANFRONTIER-EXTEND.md new file mode 100644 index 0000000..83d57e3 --- /dev/null +++ b/prompts/TRY-LEANFRONTIER-EXTEND.md @@ -0,0 +1,60 @@ +# Try LeanFrontier with an agent (extension arm) + +You are an agent preparing one ordinary LeanFrontier mathematical submission. +Your goal is a pull request that the local receiver accepts without maintainer +repair. + +Repository: `https://github.com/carlok/LeanFrontier` + +## Read first + +Read these files in order. They are the source of truth; this page is only a +short task launcher. + +1. [`CONTRACT.md`](../CONTRACT.md) — binding protocol. +2. [`prompts/SUBMITTER.md`](SUBMITTER.md) — library and submission rules. +3. [`README.md`](../README.md) — local setup and validation command. +4. The generated [catalogue](../docs/catalogue/index.html), then the source and + claim of one accepted submission that is relevant to your chosen area. + +Do not change trusted infrastructure. An ordinary submission changes only: + +- ordinary Lean source beneath `LeanFrontier/`; and +- exactly one new `Submissions/.json` claim. + +## Produce one candidate + +Start from current `main` in a fork or branch. Read the catalogue and choose an +accepted submission to build on. Import its module and prove something that +depends on it: a generalization, a consequence, or a result that needs it as a +lemma. A near duplicate is still a near duplicate and will be rejected. Write a +small, general, importable subject module with a stable mathematical namespace +below `LeanFrontier.`. + +State one or more qualified theorem entrypoints in the claim. Keep your +provenance fields accurate. Do not use `sorry`, `sorryAx`, `axiom`, unsafe or +metaprogramming commands, generated payloads, producer-specific namespaces, or +a sweep of trivial/permuted examples, including one continued from a submission +already accepted. Do not add aliases merely for a future +Mathlib migration. + +The receiver checks the elaborated declarations, including their transitive +axiom closure, exact duplicate fingerprints, baseline-only triviality probes, +and a downstream import. Passing `lake build` alone is not enough. + +## Validate before opening the pull request + +Run these commands from the repository root after fetching the target branch: + +```sh +lake build +./tools/validate-submission --base-ref origin/main --json-out .frontier/report.json +``` + +Open the pull request only if the second command exits with status zero and its +JSON says `"accepted": true`. If it rejects the candidate, read its stable +diagnostic code, revise the Lean source or claim yourself, and run the same +command again. The receiver does not repair submissions. + +When opening the pull request, keep it to this one submission. Do not bundle +documentation, workflow, policy, toolchain, prompt, test, or formatting edits. diff --git a/tests/test_launcher_arms.py b/tests/test_launcher_arms.py new file mode 100644 index 0000000..d480ed9 --- /dev/null +++ b/tests/test_launcher_arms.py @@ -0,0 +1,63 @@ +"""The launcher A/B is only interpretable if the arms differ in one place. + +Anything else that drifts between the two files becomes a second, unrecorded +treatment. See PREREGISTRATION.md. +""" + +import unittest +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +CONTROL = ROOT / "prompts" / "TRY-LEANFRONTIER.md" +EXTENSION = ROOT / "prompts" / "TRY-LEANFRONTIER-EXTEND.md" + +# The paragraph the experiment varies, plus the title line that names the arm. +CONTROL_BLOCK = """Start from current `main` in a fork or branch. Inspect the existing library and +catalogue before choosing a subject: prefer an uncovered area or a genuine +extension over a near duplicate.""" + +EXTENSION_BLOCK = """Start from current `main` in a fork or branch. Read the catalogue and choose an +accepted submission to build on. Import its module and prove something that +depends on it: a generalization, a consequence, or a result that needs it as a +lemma. A near duplicate is still a near duplicate and will be rejected.""" + + +class LauncherArms(unittest.TestCase): + def setUp(self) -> None: + self.control = CONTROL.read_text() + self.extension = EXTENSION.read_text() + + def test_each_arm_carries_its_own_block(self) -> None: + self.assertIn(CONTROL_BLOCK, self.control) + self.assertIn(EXTENSION_BLOCK, self.extension) + self.assertNotIn(EXTENSION_BLOCK, self.control) + self.assertNotIn(CONTROL_BLOCK, self.extension) + + def test_arms_are_otherwise_identical(self) -> None: + """Normalise away the varied block and the title, then compare words. + + Comparison is word-level, not byte-level: the two blocks are different + lengths, so the sentence following them rewraps. Line breaks are not a + treatment. Any difference in the words themselves is. + """ + control = self.control.replace(CONTROL_BLOCK, "").replace( + "# Try LeanFrontier with an agent", "", 1) + extension = self.extension.replace(EXTENSION_BLOCK, "<BLOCK>").replace( + "# Try LeanFrontier with an agent (extension arm)", "<TITLE>", 1) + self.assertEqual(control.split(), extension.split()) + + def test_preregistration_names_both_arms(self) -> None: + prereg = (ROOT / "PREREGISTRATION.md").read_text() + self.assertIn("TRY-LEANFRONTIER.md", prereg) + self.assertIn("TRY-LEANFRONTIER-EXTEND.md", prereg) + + def test_assignment_ledger_has_the_expected_columns(self) -> None: + rows = [l for l in (ROOT / "experiments" / "launcher-ab.csv") + .read_text().splitlines() if l and not l.startswith("#")] + self.assertEqual(rows[0], "submission_id,arm,assigned_utc") + for row in rows[1:]: + self.assertIn(row.split(",")[1], {"A", "B", "unassigned"}) + + +if __name__ == "__main__": + unittest.main()