Formal conjectures#168
Open
Shangyint wants to merge 3 commits into
Open
Conversation
Integrate google-deepmind/formal-conjectures as a git submodule (third_party/formal-conjectures, pinned to bench-v1-lean4.27.0). Each 'research open' / 'research solved' conjecture statement becomes one research-track problem (1170 problems: 349 open + 821 solved), solved by submitting a Lean 4 proof. The submodule is the single source of truth: problem directories are generated from its sources by _generator/generate.py and are NOT committed (gitignored). Run the generator once per checkout. The parser was validated against upstream's own extract_names tool (1864/1865 declarations; the one miss is an anonymous instance, warned at generation). Fill-in-the-answer statements (answer(sorry), 694) are skipped: their elaborated types substitute a placeholder for the unknown answer and would misstate the question. Evaluation: per-problem Docker image (docker/) with Lean + Mathlib + formal-conjectures prebuilt; common/fc_evaluator.py orchestrates lint -> compile -> trusted CheckDriver.lean (olean-only import, defeq statement check, axiom whitelist). Binary 1.0/0.0 score. Verified end-to-end: known proof scores 1.0; sorry / wrong statement / axiom cheat score 0.0. Framework: lean entry in LANGUAGE_CONFIGS. CI exclusion via .skip-validation marker (these problems cannot have reference solutions): detect_changed_problems, validate_problems, check_solutions (problems.txt) and the README problem count all skip them. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Instead of requiring a manual generate.py run per checkout, the framework now materializes the problem directories transparently: - ResearchRunner.get_problem_path (eval/show, all backends) and SingleEvaluator.list_problems call ensure_formal_conjectures() (src/frontier_cs/lazy_problems.py) - on first access it auto-inits the submodule if needed, runs the generator, and stamps the submodule commit in _generator/.generated-ref - when the stamp matches the submodule HEAD, access is a no-op and problems are served directly from the files; a submodule bump invalidates the stamp and regenerates Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…al-conjectures Fill-in-the-answer statements of the exact shape `answer(sorry) ↔ Q` now become problems (mode "prove_or_disprove" in target.json, 546 of them, total 1,716): the solver submits a proof of Q or of ¬Q, and the trusted CheckDriver extracts Q from the compiled `True ↔ Q` placeholder type — still never elaborating submission syntax, and failing closed to 0.0 on anything it cannot positively verify. Statements referencing section `variable`s are excluded (their compiled types gain leading ∀ binders, breaking the top-level-iff shape and making the mode ambiguous); the new _generator/shape_check.sh sweep validates every prove-or-disprove target's compiled shape in the eval image and caught 5 such cases. Value-style answers and sorry-def-tainted statements (148 total) remain excluded. Ergonomics: each problem dir now ships check.sh (one-command local scoring via docker), evaluate.sh's harness path is SOLUTION_PATH-overridable, and the readme documents local verification plus the compile-latency batching advice. The lazy-materialization stamp now includes a generate.py content hash so template changes re-materialize automatically. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Note: ENTIRELY AI GENERATED!
Summary
Adds 1,716 Lean 4 theorem-proving problems generated from the
google-deepmind/formal-conjectures
library (vendored as a submodule at
bench-v1-lean4.27.0):concrete statements; submit a
theorem solutiondefinitionally equal to thestatement.
(
answer(sorry) ↔ Q); submit a proof ofQor of¬Q.Problem directories are generated, not committed: they materialize lazily on
first
frontier list|eval|showaccess (src/frontier_cs/lazy_problems.py),stamped by submodule commit + generator hash. Scoring is binary and fail-closed:
a trusted Lean driver (
common/CheckDriver.lean) loads only compiled oleans(never elaborates submission syntax), checks definitional equality of the
solution's type (against the statement, or against
Q/¬Qextracted from thecompiled
True ↔ Qplaceholder), audits axioms, and anything it cannotpositively verify scores 0.0. Each problem dir ships a
check.shforone-command local scoring;
_generator/shape_check.shvalidates allprove-or-disprove targets on regeneration.
Known gap: the eval image
shangyint/formal-conjectures-eval:bench-v1-lean4.27.0(13.5 GB) exists only onmy machine and is not yet on Docker Hub — evaluation is not reproducible by
others until it is pushed.
Type of Change
Testing
sorry/ wrong statement /forbidden-axiom cheat → 0.0.
accepts proofs of
Qand of¬Q; rejects wrong types, non-iff targets,unknown modes; legacy invocation unchanged.
(
Erdos326.erdos_326→ 0.0 "proves neither"). A full-evaluator 1.0 in thismode has NOT been exercised — every such problem is a genuine research
question; the accept path is covered at the driver level only.
exactly
True ↔ Q(the sweep caught and excluded 5 section-variablestatements that would have been permanently zero).
claude -prun on a random problem(infrastructure exercised end-to-end; no solve, as expected).
Checklist
and shape-check procedure)
CI Validation (for new problems)
No — intentionally not applicable. These problems carry a
.skip-validationmarker and include no
reference.py: they are open (or research-grade solved)conjectures, so no reference solution scoring > 0 can exist. They are likewise
excluded from
research/scripts/problems.txtand the README problem count.