THROWAWAY: smoke-run the 2026-08-25 autoformalization target problems (misformalization check) - #29
Closed
tadamcz wants to merge 1 commit into
Closed
THROWAWAY: smoke-run the 2026-08-25 autoformalization target problems (misformalization check)#29tadamcz wants to merge 1 commit into
tadamcz wants to merge 1 commit into
Conversation
…s as erdos subset target18 18 Erdős problems (20 statements; 713 and 1206 have two parts each) from epoch-research/autoformalization results/2026-08-25-erdos-target-run, autoformalized and gate-passed at FC 9cbe1d3c (an ancestor of this dataset's 488aade2 pin; same toolchain and Mathlib, no touched shared-lib declaration is used by these files -- representative specs compile-checked in the FC image). Sources/ are the run's output verbatim; Isolated/ specs strip the @[category ...] attributes and sibling part statements, matching the existing isolation shape. Smoke-run purpose only: these are open problems formalized outside FC review, so a solve at a modest budget flags likely misformalization. Not for merge; stacked on the bloom-erdos-selection branch (PR #28).
Collaborator
Author
Smoke run launchedEval set:
Interpretation: every statement here is an open Erdős problem autoformalized outside FC review. Any Status: |
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.
Do not merge. Throwaway branch stacked on #28 for a single smoke run.
Vendors the 18 Erdős problems from the 2026-08-25 autoformalization target run (
epoch-research/autoformalizationresults/2026-08-25-erdos-target-run: 17 gate-passingsubmit/problems + 1020 fromhold/) intoapn/data/erdosas subsettarget18— 20 statements, since 713 and 1206 each have two parts, one sample per statement per the dataset's convention.Purpose: these are open problems autoformalized outside FC review. Claude Fable 5 and GPT 5.6 Sol each attempt every statement at a $50/sample cap (
configs/erdos-target18-smoke.yaml, one eval set, 40 samples, $2,000 max). Any solve at this budget is a red flag for misformalization (statement too easy / vacuous), not a result.Pin note: the run's files were produced and gate-checked at FC
9cbe1d3c, an ancestor of this dataset's488aade2pin (one day apart; same toolchain and Mathlib, no shared-library declaration touched between the pins is used by these files). Representative isolated specs — including both surgically part-split ones — compile cleanly in the FC image. The existingfc_488aade2sandbox images in ECR are reused as-is.Isolation-certificate tests were not updated for the new files (throwaway branch); expect CI to be red.