Pre-register the launcher A/B and add the extension arm - #136
Merged
Conversation
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
The launcher currently tells producers to "prefer an uncovered area", which points away from the corpus. So LeanFrontier's 0.17 internal import edges per module may be an artifact of our own instruction rather than a property of machine-generated mathematics.
Measured today against Tau Ceti, at a matched 24 modules and with no subsampling:
Per module p = 2.7e-4. Per declaration the gap is 2.20x with 95% CI [0.75x, 8.80x], p = 0.096 — not established at these counts. Tau Ceti's density rises monotonically to 1.55 by 2314 modules, so machine-generated mathematics does accumulate there; it is also directed by human-written roadmaps, which is what this experiment separates.
Method and scripts:
carlok/lean-corpus-density.What this adds
PREREGISTRATION.md— hypothesis, metric, decision rule and limitations, fixed before any submission is assigned.prompts/TRY-LEANFRONTIER-EXTEND.md— arm B, differing from arm A in exactly one paragraph.experiments/launcher-ab.csv— arm assignment, recorded at invitation.tests/test_launcher_arms.py— asserts the arms stay word-identical outside the varied block, so nothing drifts in as a second unrecorded treatment.Stopping point is 18 accepted submissions per arm: 0.93 power against a Tau-Ceti-sized effect, 0.82 against 4x, and the pre-registration says in advance that a null means "no effect larger than ~4x", not "no accumulation".
Not changed
No receiver behaviour, no policy, no schema.
prompts/TRY-LEANFRONTIER.mdis untouched — it is the control arm. Generators are at a fixed point; 90 tests green.