Standardize dataset storage on JSONL manifests - #19
Merged
Conversation
One SampleRow schema and one loader across the three datasets: samples.jsonl (id, vendored source path, optional exclusion reason, dataset extras) replaces the per-dataset mapping/membership txt parsers, and subsets/<name>.json replaces the OEIS-only txt subsets. Sample.metadata is built from an explicit whitelist so manifest-only fields (recorded-verdict material) never reach the agent. Data conversion of the three datasets follows.
Auto/ becomes Sources/ (uniform vendored-tree name; its README records the upstream pin), samples.jsonl transcribes upstream's THEOREM_MAPPING.txt (deleted; sha256 recorded in NOTICE.md, transcription verified byte-verbatim against the pinned clone), oeis_id is materialized per row, and the three subsets become subsets/<name>.json with their rationale as descriptions -- lite's id set is unchanged by construction (seeded draw over sorted ids, asserted at conversion).
samples.jsonl carries all 100 members of the paper's frozen subset -- the 14 value-typed answer(sorry) members as excluded rows with the reason inline -- replacing FC100OpenSet1.lean + MAPPING.txt + EXCLUDED.txt (membership file's sha256 recorded in NOTICE.md; transcription verified byte-verbatim against the pinned clone). The 12 source files hosting only excluded targets are now vendored so every row's source resolves, and the generator re-verifies each exclusion against the elaborated statement (sorryAx in its type).
The dataset is now defined by FC, not by the Tsoukalas paper: samples.jsonl censuses every research-category statement in the vendored ErdosProblems tree at the pin (1124 rows; Sources/ grows 236 -> 420 files), and the paper's canonical 350-statement attempted set becomes subsets/tsoukalas_attempted.json (ATTEMPTED/EXCLUDED/RENAMED/MAPPING.txt deleted; upstream hash and the 353->350 derivation live in the subset description; resolution verified identical to the old mapping, and the previously shipped 350 specs are byte-identical after regeneration). Universe rows record erdos_number, category_at_pin, and answer_form (kept out of sample metadata -- they encode the recorded verdict). 103 members ship as excluded rows: 79 value-typed answer(sorry) (sorryAx in the statement type) and 24 whose complete formal proof is in the source file. The answer(...) <-> machinery gains the filled-RHS forms 198.lean introduced (rhs_true/rhs_false), the sorry allowlist becomes file-scoped (295/633/697/961/1055 keep a sorry'd helper their definitions need), and one case-insensitive filename collision (889's V1/v1 variants) is carried by an explicit per-row statement path. A six-agent leak audit of the 671 new specs extended the verdict-prose strip with the DeepMind/AlphaProof channel; the broader cleanup of resolution prose on post-paper solved members is deferred and documented in NOTICE.md.
The oeis/fc100 fast suites and all three isolation suites enumerate from samples.jsonl instead of the deleted mapping files (the erdos structural gate also cross-checks each row's recorded answer_form against the source's re-detected form), and the OEIS analysis/fetch scripts read their sequence universe from the manifest.
raw/ said nothing about what the directory meant, and the OEIS enrichment tables sat loose at the dataset root, indistinguishable from the dataset proper. Each dataset now has one metadata/ tree for data *about* the members (analysis-only; a README notes none of it reaches Sample.metadata): snapshots/ for captures of external sources (unreproducible, read-only evidence -- the old raw/) and derived/ for tables our scripts compute (provenance and the two citations files, prefixes dropped now that the directory carries the context). The distinguishing axis is snapshot vs derived, not fetched vs computed: the OpenAlex citations are also fetched, but they are our query-and-join synthesis, not a capture.
Collaborator
Author
CI's isolation gate caught three new-member specs broken by constructs the dependency cut cannot see: type_of% splices a sibling's elaborated *type*, so the sibling never appears in the extractor's deps and the cut removed the statement being referenced (11.variants.granville_soundararajan, 392.variants.implication), and 683.lean/1145.lean import another problem file, whose olean the sandbox images do not build -- 1145's importer is its @[category test] sibling, which the cross-file reference makes entirely invisible to the extractor, so it survived the cut as gap trivia. HARDCODED_ISOLATION applies exact per-member text replacements at generation: the referenced sibling statements are inlined verbatim where type_of% stood (hypotheses, not sorry'd theorems -- SafeVerify would otherwise demand their proofs), and the dead cross-file imports (plus 1145's invisible sibling and 683's namespace open) are dropped. Generation now also rejects any spec that imports a problem module or type_of%-references a declaration outside itself, so the failure modes cannot recur silently. All seven re-verified in the container: re-extraction, the type certificate (which checks the hand-inlined types against Lean's own elaboration of the source), and the compile gate.
This reverts commit af18018.
The full-FC-universe expansion brought in members the isolation pipeline cannot ship without hand-editing: cross-problem-file imports (683, 1145), type_of% statement splices (11, 392), one member the extractor cannot see at all (1135's type_of% on an imported sorry'd theorem never reaches the env diff), and a census miss for 509's doc-comment-glued research attribute. Rather than hand-isolating or excluding them piecemeal, the universe returns to the Tsoukalas paper's canonical 350 attempted statements: samples.jsonl is filtered to the tsoukalas_attempted ids (pure row deletion; every kept row and all 350 specs byte-identical), Sources/ returns to the 236 hosting files (exactly main's vendored set), and there are no excluded rows. The manifest format, subsets mechanism, and metadata/ are unchanged. generate_erdos_isolated.py remains the vendor-time bootstrap; it censuses all of Sources/, so the committed manifest is now explicitly curated (NOTICE.md documents this and the three attempted members still carrying resolution material: Erdos1141 and Erdos318.parts.ii state their recorded verdict and link the published solution, Erdos997 keeps the solution paper's reference line -- shipped as-is for now). The fc100open NOTICE's tag-vs-pin paragraph is corrected: exactly three of the 88 problem files differ, and the moved defs belong to Equidistribution.lean, not GraphConjecture316.lean (byte-identical at both).
PR #20's files land in this branch's metadata/ layout: the wiki-page scrape under metadata/snapshots/, the derived profiles under metadata/derived/; scripts/extract_proposers.py's paths follow (incl. conjecture_provenance.jsonl -> metadata/derived/provenance.jsonl) and the metadata README lists the new files.
tadamcz
changed the title
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.
Format
Every dataset under
apn/data/<ds>/has the same shape:samples.jsonl— the membership source of truth, one row per sample:id,source(vendored file path), optionalexcluded(reason inline; only dataset/harness-intrinsic reasons), optionalstatement(spec-path override), plus dataset extras (oeis_id,erdos_number,category_at_pin,answer_form).Isolated/<id>.lean— the shipped specs.Sources/— vendored Lean, verbatim, one name across datasets; each tree carries a README recording the exact upstream pin.subsets/<name>.json—{description, ids}; every id must exist in the manifest; derivation stories (upstream lists, seeds, renames) are prose indescription. All datasets share the mechanism and thesubsettask arg.metadata/(oeis, erdos) — data about the problems (scrape snapshots, derived provenance/citations), with its own READMEs.NOTICE.md— the dataset-level story; no repeated pins.Vendoring rule: verbatim only when CI must read the bytes (Lean sources) or the upstream is not durably addressable (scrapes). Upstream control files are transcribed rather than vendored — oeis
THEOREM_MAPPING.txt, fc100openFC100OpenSet1.lean, the erdos attempt lists — with their sha256 at the pinned commits recorded in the NOTICEs / subset descriptions; each transcription was verified byte-verbatim against the pinned clones.apn/dataset.pycollapses to one loader (load_manifest/load_subset/build_dataset);Sample.metadatais built from an explicit whitelist so manifest-only fields (category_at_pin,answer_form— the recorded verdict in machine-readable form) never reach the agent.Datasets
lite,tsoukalas_proved_38,tsoukalas_unproved_40ship assubsets/*.json; the multi-formalization metadata key is nowother_sources.metadata/holds the OEIS/OpenAlex scrape snapshots and derived provenance/citation tables.answer(sorry)excluded): membership transcribed from the paper's frozenFC100OpenSet1.lean. The NOTICE records tag-vs-pin comparability: of the 88 problem files, exactly three differ betweenbench-v1-lean4.27.0and the pin — two doc-comment-only, one whose twodefs moved verbatim intoFormalConjecturesForMathlib.erdos_number/category_at_pin/answer_formfor tooling;subsets/tsoukalas_attempted.jsonnames the same 350 ids — the canonical replication invocation (the 353→350 derivation, upstream commit and hash live in its description) — and bareapn_erdosruns them all. The NOTICE documents the answer-key hygiene mechanism (certifiedanswer(...) ↔rewrite; category/verdict-prose strip) and flags the three members whose doc comments still carry resolution material (Erdos1141.erdos_1141,Erdos318.erdos_318.parts.ii,Erdos997.erdos_997), shipped as-is. The committed manifest is curated:generate_erdos_isolated.pycensuses every research-category statement inSources/, and the manifest keeps the attempted subset of that census.Continuity guarantees (verified)
main(checked via a worktree dump comparison)..txtlist it replaces (lite,proved_38,unproved_40, and the attempted 350 vsMAPPING.txt).