Formal conjectures

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "third_party/formal-conjectures"]
+	path = third_party/formal-conjectures
+	url = https://github.com/google-deepmind/formal-conjectures.git

CONTRIBUTING.md

@@ -362,3 +362,58 @@ Please include:
 - Area of expertise
 - Type of contribution (algorithmic/research problem)
 - Brief description of your proposed contribution
+
+## Formal Conjectures (Lean) Problems
+
+`research/problems/formal_conjectures/` hosts one problem per conjecture
+statement from [google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
+(categories `research open` and `research solved`). The source of truth is the
+git submodule at `third_party/formal-conjectures`, pinned to a `bench-*`
+release tag; **problem directories are generated from it and are not
+committed** (see the `.gitignore` there). Materialization is automatic: the
+first `frontier list|eval|show` touching these problems initializes the
+submodule and runs the generator (`src/frontier_cs/lazy_problems.py`), stamping
+the submodule commit plus a generator hash in `_generator/.generated-ref` so
+later accesses serve the files directly (and template changes in `generate.py`
+re-materialize automatically). To materialize manually:
+
+```bash
+git submodule update --init third_party/formal-conjectures
+python3 research/problems/formal_conjectures/_generator/generate.py
+```
+
+- The generator parses the submodule's Lean sources directly (namespaces,
+  `@[category ...]` attributes) — no Lean toolchain needed. "Fill-in-the-answer"
+  statements (`answer(sorry)`) elaborate with a placeholder (`True` for Props),
+  so the plain "prove this" contract would misstate them. Those of the exact
+  binder-free shape `answer(sorry) ↔ Q` become mode `prove_or_disprove`
+  problems (submit a proof of `Q` or of `¬Q`; the trusted checker extracts `Q`
+  from the compiled `True ↔ Q` type and fails closed on anything else). The
+  rest — value-style answers, statements referencing section `variable`s or
+  sorry-containing defs — are skipped rather than misrepresented. After a
+  submodule bump, validate with
+  `research/problems/formal_conjectures/_generator/shape_check.sh` (requires
+  docker + the eval image): it rechecks every prove-or-disprove target's
+  compiled shape.
+- Solutions are Lean 4 proofs, checked in a Docker image with Lean + Mathlib +
+  formal-conjectures prebuilt (`research/problems/formal_conjectures/docker/`).
+- Scoring is binary: 1.0 iff the submitted proof compiles without `sorry`,
+  proves a statement definitionally equal to the conjecture, and uses only the
+  standard axioms. See `research/problems/formal_conjectures/common/`.
+- These problems are **excluded from CI validation** (the `.skip-validation`
+  marker): open conjectures cannot have a reference solution scoring > 0.
+  They are also excluded from `research/scripts/problems.txt` and the README
+  problem count.
+
+To bump the submodule to a new upstream release:
+
+```bash
+git -C third_party/formal-conjectures checkout <new-bench-tag>
+research/problems/formal_conjectures/docker/build.sh --push   # rebuild eval image
+python3 research/problems/formal_conjectures/_generator/generate.py --wipe
+git add third_party/formal-conjectures                        # only the pointer changes
+```
+
+The parser can be cross-checked against upstream's own extractor:
+`docker run --rm <eval-image> lake exe extract_names > /tmp/extract.json`
+then `generate.py --check-against /tmp/extract.json`.

research/README.md

@@ -35,9 +35,9 @@ frontier batch research --status           # Check progress
 ## Python API
 
 ```python
-from frontier_cs import SingleEvaluator
+from frontier_cs import SingleEvaluator
 
-evaluator = SingleEvaluator()
+evaluator = SingleEvaluator()
 
 # Single problem (uses SkyPilot by default for research)
 result = evaluator.evaluate("research", problem_id="flash_attn", code=my_code)
@@ -135,3 +135,27 @@ class Solution:
 
 Check each problem's `readme` for the specific `solve()` signature and return type.
 
+
+## Formal Conjectures (Lean) Problems
+
+`formal_conjectures/<source>/<theorem>` problems ask for a Lean 4 proof of a
+formalized conjecture from
+[google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures).
+Problem directories are generated from the `third_party/formal-conjectures`
+submodule and are not committed — the framework materializes them
+automatically on first access (list/eval/show):
+
+```bash
+# List them (generates the problem dirs on first run)
+uv run frontier list research | grep formal_conjectures
+
+# Evaluate a proof (Docker backend; the image bundles Lean + Mathlib prebuilt)
+uv run frontier eval research formal_conjectures/erdos_problems/Erdos1.erdos_1 \
+    proof.lean --backend docker
+```
+
+A submission is a single Lean file declaring a top-level
+`theorem solution : <exact statement> := <proof>` (see each problem's readme).
+Score is binary: 1.0 iff the proof compiles without `sorry`, the statement
+matches the conjecture up to definitional equality, and no axioms beyond
+`propext`, `Classical.choice`, `Quot.sound` are used.

research/problems/formal_conjectures/.gitignore

@@ -0,0 +1,8 @@
+# Problem directories are generated from the third_party/formal-conjectures
+# submodule and are not committed. Materialize them with:
+#   python3 research/problems/formal_conjectures/_generator/generate.py
+/*/
+!/_generator/
+!/common/
+!/docker/
+/_generator/.generated-ref

research/problems/formal_conjectures/.skip-validation

@@ -0,0 +1,3 @@
+Problems in this directory are auto-generated Lean proof tasks for open math
+conjectures. Open conjectures cannot have a reference solution scoring > 0,
+so CI reference validation is skipped (see scripts/detect_changed_problems.py).

research/problems/formal_conjectures/_generator/ShapeCheck.lean

@@ -0,0 +1,47 @@
+/-
+Validation sweep for prove-or-disprove problems (run via shape_check.sh).
+
+Reads a file of lines "<module components> / <theorem components>" and checks,
+in the prebuilt eval environment, that every target's compiled type has the
+exact placeholder shape `True ↔ Q` required by CheckDriver.lean's
+"prove_or_disprove" mode. Any target failing this would be a permanently-zero
+problem (the driver fails closed) and must be excluded by the generator —
+typically because the statement references section `variable`s, which prepend
+∀ binders to the compiled type.
+
+Prints one "BAD <reason>: <name>" line per failure and a final
+"checked <n>, bad <m>" summary; exits non-zero iff any target is bad.
+-/
+import Lean
+open Lean
+
+def mkNameFromComponents (cs : List String) : Name :=
+  cs.foldl .str .anonymous
+
+def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let lines ← IO.FS.lines ⟨args.head!⟩
+  let entries := lines.filterMap fun l =>
+    if l.isEmpty then none
+    else
+      match l.splitOn " / " with
+      | [m, t] => some (mkNameFromComponents (m.splitOn " "),
+                        mkNameFromComponents (t.splitOn " "))
+      | _ => none
+  let mods := entries.map (fun e => ({ module := e.1 } : Import))
+  let env ← importModules mods {}
+  let mut bad := 0
+  let mut total := 0
+  for (_, name) in entries do
+    total := total + 1
+    match env.find? name with
+    | none => IO.println s!"BAD missing: {name}"; bad := bad + 1
+    | some ci =>
+      if ci.type.hasSorry then
+        IO.println s!"BAD hasSorry: {name}"; bad := bad + 1
+      else if !ci.type.isAppOfArity `Iff 2 then
+        IO.println s!"BAD not-iff: {name}"; bad := bad + 1
+      else if !(ci.type.appFn!.appArg!.isConstOf `True) then
+        IO.println s!"BAD lhs-not-True: {name}"; bad := bad + 1
+  IO.println s!"checked {total}, bad {bad}"
+  return if bad == 0 then 0 else 1