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()