Add the erdos_autoformalized dataset - #30
Merged
Merged
Conversation
18 Erdős problems formalized by our own autoformalization pipeline (epoch-research/autoformalization, results/2026-08-25-erdos-target-run), absent from formal-conjectures at the run's pin -- the first dataset not vendored from upstream FC (see the dataset's NOTICE.md). This commit carries the machinery: the verbatim vendored Sources/ (the run's root .lean files: banners dropped, answer-iff forms already rewritten), the fc_commit pin 9cbe1d3c (what the run compiled against; registered in _FC_PROFILES), the apn_erdos_autoformalized task + dataset builder, the vendor-time generator (no un-recording surgery: it asserts the shipping-form invariants instead of rewriting/excluding), the validation suites, and the CI wiring. The generated samples.jsonl + Isolated/ land in the next commit.
scripts/generate_erdos_autoformalized_isolated.py output, run in the Dockerfile generate stage at the dataset's pin (9cbe1d3c): 20 manifest rows (the 18 problems; 713 and 1206 are two-part) and their per-target Isolated/ specs -- sibling parts cut, @[category ...] lists dropped (20 stripped). Every source elaborated cleanly, and all 20 specs compile with the scorer's exact `lake env lean -o` command in the same container.
tadamcz
commented
Aug 26, 2026
tadamcz
commented
Aug 26, 2026
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/erdos_autoformalized: the 18 Erdős problems formalized by our own autoformalization pipeline (epoch-research/autoformalization,results/2026-08-25-erdos-target-run), absent from formal-conjectures at the run's pin. This is the first dataset not vendored from upstream FC — the dataset'sNOTICE.mddocuments provenance and how that changes the usual layout semantics..leanfiles, verbatim (banners dropped andanswer(sorry) ↔forms already rewritten upstream of this repo). Problem 1020 (gate-held in the run over a decomposition dispute, not the formalization) is included on the same footing as the rest; no gate distinction is recorded.9cbe1d3c— the FC commit the pipeline compiled against (post-rename layout, Lean v4.27.0; an ancestor of the erdos dataset's488aade2), registered in_FC_PROFILES. Since nothing is vendored from FC, the pin plays only its runtime role (sandbox images + proving-library version).scripts/generate_erdos_autoformalized_isolated.py(the shared cut engine; no un-recording surgery — the shipping-form invariants are asserted instead of rewritten). 20 members over 18 files: 713 and 1206 are two-part, one sample per part with the sibling cut.apn_erdos_autoformalized(no subsets; the default runs all 20).tests/test_erdos_autoformalized.py(cheap census/shape/textual invariants) andtests/test_erdos_autoformalized_isolation.py(container suite: re-extraction structural check with the plain-equality statement certificate, and the scorer-exact compile gate), wired into the CI isolation job.Locally verified at the pin: every source elaborates cleanly, all 20 specs compile with the scorer's exact
lake env lean -o, cheap tests + mypy pass.