Add the wikipedia_autoformalized dataset - #47
Draft
tadamcz wants to merge 3 commits into
Draft
Conversation
…ck, batch JSON Four fixes to the shared vendor-time/test tooling, surfaced by the wikipedia_autoformalized sources (the first dataset whose files carry substantial definitions with proof arguments, native-decide sanity checks and multi-universe statements): - ExtractRanges: `deps` now looks through the elaborator's unranged auxiliaries (a definition's `_proof_N` abstractions, matchers, well-founded-recursion helpers) to the source-ranged declarations they use, so a lemma referenced only inside a definition's proof argument (a Quotient.lift congruence proof, a Finset.sup' nonemptiness proof) counts as that definition's dependency. Without it the isolation cut removed lemmas kept definitions needed: 40 wikipedia_autoformalized specs did not compile. erdos_autoformalized regenerates byte-identically with the new extractor, and the erdos + erdos_autoformalized isolation suites pass. - CertifyDisproof: universe parameters are compared up to reordering. `type_of%` re-generalizes them by occurrence, so a three-universe target (Fujita's conjecture) had its disproof's parameters permuted and the positional canonicalization rejected a correct negation. - scripts/isolation.py `lake_env_command`: the extractor and certifier run with an unlimited stack -- a `decide +native` sanity example over a large finite search overflows the default 8 MiB in the exe's interpreter, while `lean` itself elaborates on a larger thread stack -- with optional gzipped stdout-to-file. The compile gate deliberately keeps the scorer's conditions. - tests/lean_sandbox.py: the JSON tools run in batches of 10 files, 6 concurrently, gzipped to a file and read back through `read_file`. Inspect caps an exec's stdout at 10 MiB and a `read_file` at 100 MiB; one call over all 243 sources exceeded the former and a 25-file batch the latter (KazhdanLusztigConjectures.lean's 16 theorems print to 242 MB of elaborated types, gzipping to a few MB).
Wikipedia's "List of unsolved problems in mathematics" entries formalized by our own autoformalization pipeline (epoch-research/autoformalization, Hawk eval set autoformalize-full-r8zuxgce3jf7ppre, 2026-09-03), absent from formal-conjectures at the run's pin -- the second dataset not vendored from upstream FC (see the dataset's NOTICE.md). Selection, by the new scripts/vendor_wikipedia_autoformalized.py: a sample's final file is vendored verbatim iff its headline `formalized` score is CORRECT or PARTIAL and the adjudicator's confidence is >= 0.8 -- 248 of the run's 335 samples; 5 of those import a sibling FC problem module the sandbox images do not carry and are not vendored, leaving 243 files. metadata/run_samples.jsonl records every run sample's outcome (score, confidence, kept slots, probe, selection, vendored file or reason) and metadata/run.json the run's identity; both are written by the vendor script. fc_commit is the run's FC pin 9cbe1d3c (already registered; images shared with erdos_autoformalized). This commit carries the machinery: the apn_wikipedia_autoformalized task (default subset `adjudicated_open`) + dataset builder, the isolation frontend, the generator (the Erdős census: every research-category theorem is a member; value-typed answer(sorry) members become excluded rows; kept slots must resolve to members; every stripped @[category ...] list must be a plain classification list), the fast and container test suites, the CI wiring and the layout note. The generated samples.jsonl, Isolated/ and subsets/ land in the next commit.
…fault subset scripts/generate_wikipedia_autoformalized_isolated.py output at the dataset's pin (9cbe1d3c), run in the apn-isolate-dev container with the in-tree build of the extractor: 432 manifest rows (354 research open, 78 research solved) of which 15 value-typed answer(sorry) statements are excluded rows, and 417 isolated specs -- siblings and examples cut, 127 `answer(sorry) ↔` and 3 recorded `answer(False) ↔` forms rewritten to plain P, 619 @[category ...] lists dropped, the derived `.disproof` appended. The 356 kept slots of the run's adjudicator all resolve to members (38 of them classified research solved, 12 value-typed). subsets/adjudicated_open lists the 305 kept slots that are research open, scoreable and record no verdict (over 226 problems) -- leaving out the research-solved kept slots, the formalizers' non-adjudicated variants, and the Connes embedding problem, stated `answer(False) ↔ P` after MIP* = RE. All 417 specs pass the container suite: the cut prediction and rewrite certificates, no surviving examples, disproof certification, and the scorer's exact `lake env lean -o` compile.
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.
Adds
apn/data/wikipedia_autoformalized: the Wikipedia List of unsolved problems in mathematics entries formalized by our own autoformalization pipeline (epoch-research/autoformalization, Hawk eval setautoformalize-full-r8zuxgce3jf7ppre, 2026-09-03), absent from formal-conjectures at the run's pin — the second dataset not vendored from upstream FC. The dataset'sNOTICE.mddocuments provenance;metadata/run.jsonrecords the run's identity and task args.answer(sorry)adjudicated_open, over problemsscripts/vendor_wikipedia_autoformalized.py): a sample's final file is vendored verbatim iff its headlineformalizedscore is CORRECT or PARTIAL and the adjudicator's confidence is ≥ 0.8 — 248 of the run's 335 samples. 5 of those import a sibling FC problem module the sandbox images do not carry and are not vendored (giuga-number, euler-equations, linniks-theorem, ramanujan-petersson-conjecture, unknotting-problem), leaving 243 Sources/ files.metadata/run_samples.jsonlrecords every run sample's outcome: score, confidence, kept slots, probe result, selection, vendored file or the reason it was not.9cbe1d3c, shared with erdos_autoformalized (already registered; images shared).scripts/generate_wikipedia_autoformalized_isolated.pywith the Erdős census (every research-category theorem is a member): 432 rows (354 research open, 78 research solved), 15 value-typedanswer(sorry)statements as excluded rows, 417 specs. 127answer(sorry) ↔and 3 recordedanswer(False) ↔forms are rewritten to plainP(certified by re-elaboration). Each row carries the run facts —problem_id,title,slotfor the adjudicator's 356 kept slots,formalized,adjudicator_confidence,answer_form— none of which reach sample metadata.subsets/adjudicated_open.jsonlists the 305 kept slots that are research open, scoreable and record no verdict, over 226 problems. It leaves out the 38 research-solved kept slots, the formalizers' non-adjudicated research variants, and the Connes embedding problem (statedanswer(False) ↔ Pafter MIP* = RE while still classified research open). It isapn_wikipedia_autoformalized's default;subset=Noneruns the full manifest.depsnow look through the elaborator's unranged auxiliaries, so a lemma used only inside a definition's proof argument counts as that definition's dependency (40 specs otherwise lost lemmas their definitions needed and did not compile; erdos_autoformalized regenerates byte-identically); the disproof certifier compares universe parameters up to reordering (Fujita's three-universe statement); the extractor and certifier run with an unlimited stack (adecide +nativesanity example overflowed the default — the compile gate deliberately keeps the scorer's conditions); the container suites batch and gzip the tools' JSON through a file (Inspect caps exec stdout at 10 MiB andread_fileat 100 MiB; one file's elaborated types print to 242 MB).tests/test_wikipedia_autoformalized.py(census, run-table consistency, subset, shape, textual invariants) andtests/test_wikipedia_autoformalized_isolation.py(container suite: cut prediction + per-form rewrite certificates, no surviving examples, disproof certification, scorer-exact compile), wired into the CI isolation job.Locally verified at the pin: all 417 specs pass the container suite; the erdos and erdos_autoformalized isolation suites pass with the tooling changes; cheap tests + mypy pass. The oeis and fc100open isolation suites were not run locally (CI runs them; the extractor change cannot alter their committed specs without having broken their compile gates before).
Judgment calls to review: the census universe with a default subset (vs. kept slots only); excluding recorded-verdict statements from the default subset; not vendoring the 5 sibling-import files; keeping the research-solved kept slots in the manifest.