Switch the Erdős dataset to the Bloom statement selection - #28
Merged
Conversation
…tion Vendors Thomas Bloom's statement-selection review doc and the migration plan: pin erdos at FC 488aade2 (last v4.27.0 commit; all 48 selected declarations identical to review commit 56534c04), parameterize generic code by FC commit for the FormalConjecturesUtil rename, ship 508 as a value-typed exclusion (47 runnable). Gate B (new-pin image smoke: build, compile, safe_verify, extractor) already run and passed; results recorded in the plan.
Both formal-conjectures repo layouts must be supported simultaneously: the erdos pin is about to move past upstream's FormalConjecturesUtil rename while oeis/fc100open stay at the old-layout pin. - apn/dataset.py: FCProfile registry keyed by pin; fc_profile() fails loudly on unregistered pins. - apn/lean/Dockerfile: builder guards the lean-toolchain invariant, detects the layout from the checkout (the ground truth) for the lake build, and stages the proving-library sources into /staged so the base stage's COPY needs no branch. - extract_ranges: the util module is a required --util-module CLI flag (no default), threaded through run_extractor / lean_sandbox.extract and all generator/test callers via fc_profile(). - prompts/solver/task: user_prompt names the pin's util module in the import-integrity rule instead of a hardcoded one. All pins unchanged; pure refactor (Gate A rides on the existing suites).
…urces C1/C2/C6 of the migration plan: fc_commit moves to the last FC commit on Lean v4.27.0 (21 commits before the review commit 56534c04, which is on v4.33.1); the 236 Tsoukalas-era Sources/*.lean are replaced by the 48 files hosting Bloom's selected statements; the selection doc moves to its permanent home under apn/data/erdos/metadata/. scripts/erdos_statement_certificate.py is the auditable link between the vendored pin and the review commit: it certifies every selected declaration command byte-identical between the two (vendor-time run: 48/48; residual non-statement diffs in 8 files), and that the vendored copies match FC at the pin. Result recorded in NOTICE.md. samples.jsonl and Isolated/ still reflect the old dataset; they are regenerated in the next commits (C4).
…lection C3/C5/C7 + workstream D of the migration plan: - scripts/erdos_isolation.py: SORRY_ALLOWLIST_FILES emptied (no Bloom file needs one); VERDICT_PROSE pruned to the one snippet the 48 files still contain (138.variants.difference's recorded-verdict prose), after auditing every research-solved member's doc against the new sources. - apn_erdos defaults to subset="bloom_selection" (47 scoreable selected statements); subset=None remains the whole census. Docstrings rewritten. - tests/test_erdos.py: census invariants for the new universe (one row per research statement of the 48 files; 508 + 975.variants.quadratic value- typed, 647.variants.twenty_four proved-in-file; per-form counts; the selection all research-open; sketch invariants unchanged in spirit). - tests/test_singlefile_proof.py: end-to-end accept case in the erdos pin's scorer image (institutionalizes the pin-move smoke test: compile + kernel replay against the module-built FormalConjecturesUtil oleans). samples.jsonl, Isolated/, and subsets/bloom_selection.json are regenerated in the next commit (C4/C5); test_erdos.py census constants are asserted against that output.
C4/C5 of the migration plan, produced by generate_erdos_isolated.py in the generate container at 488aade2 (with the extractor's new required --util-module flag; a Lean parse fix to its usage error rides along): - samples.jsonl: 144 universe rows -- every research-category statement of the 48 vendored files. 3 excluded: Erdos508.HadwigerNelsonProblem and Erdos975.erdos_975.variants.quadratic (value-typed answer(sorry)), Erdos647.erdos_647.variants.twenty_four (complete in-file proof). - Isolated/: 141 per-target specs; answer forms 87 plain / 52 lhs_sorry / 2 lhs_true (the recorded verdicts un-filled), 141 category attribute lists and 1 verdict-prose snippet stripped. - subsets/bloom_selection.json: the 47 scoreable selected statements (apn_erdos's default subset), in problem-number order. - tests/test_erdos.py: answer-form census pinned to the generated output. Fast suites + mypy green; the container gates (test_erdos_isolation.py, test_singlefile_proof.py) run in CI.
Collaborator
Author
|
Smoke run on the new dataset: erdos-bloom-opus5-100usd — the 47-sample |
tadamcz
commented
Aug 26, 2026
tadamcz
marked this pull request as ready for review
August 26, 2026 10:42
tadamcz
added a commit
that referenced
this pull request
Aug 26, 2026
Both sides' intents compose: - apn/data/erdos: main's regenerated Bloom-selection dataset (pin 488aade2, 144-row manifest, 141 specs) wins wholesale; the branch's append_disproof post-step (comparator-migration-plan.md §4) is then re-applied to every spec, exactly as scripts/generate_erdos_isolated.py does after extraction (83 specs appended; the 58 the auto-merge already composed verified byte-identical to the derivation). - apn/task.py: Comparator scorer + backend-parameterized sandbox config (ours) over main's fc_profile-threaded pin. - apn/lean/Dockerfile: main's toolchain guard, util-module layout detection and /staged staging, composed with the comparator/lean4export/landrun stages; the Challenge/Solution stub imports are now layout-detected too. - CertifyDisproof.lean gains the same required --util-module flag main gave ExtractRanges (its ProblemImports import was hardcoded, which would fail at the post-rename erdos pin); tests/lean_sandbox.py::certify and the three isolation suites thread it through. - tests/test_singlefile_proof.py: the shared module-scoped comparator env (ours) with _comparator_env/_spec parameterized by pin, and main's institutionalized erdos-pin accept smoke test translated to the comparator checker. - scripts/comparator_drift.py: the pinned candidate set re-censused for the new corpus -- 3 confirmed private rejects (Erdos340 x3) and 2 candidates (Erdos1141, Erdos1148) left with the Tsoukalas-era files; Erdos101 remains. mypy + the fast suite green; the container gates run in CI.
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.
No description provided.