Add LiveProveBench runner driver

config/config_liveprovebench.yaml

@@ -0,0 +1,46 @@
+# Shared settings for LiveProveBench runs.
+# Per-problem rows (name + paths) live in ../../lists.txt.
+#
+# Run the first 3 problems, 10-minute pause between each:
+#   python scripts/run_liveprovebench.py --count 3 --sleep-between 10
+#
+# Resume (e.g. continue from #4):
+#   python scripts/run_liveprovebench.py --from 4 --count 3 --sleep-between 10
+#
+# Dry-run (preview without executing):
+#   python scripts/run_liveprovebench.py --dry-run --count 3 --sleep-between 10
+
+lean_repo: /mnt/nvme1/jacky/workspace/_eval_lb/LiveProveBench
+lists_file: /mnt/nvme1/jacky/workspace/_eval_lb/numina-lean-agent/config/lists.txt
+# Paths inside lists.txt are resolved against this base.
+lists_base: /mnt/nvme1/jacky/workspace/_eval_lb
+
+prompt_template: prompts/prompt_hard_mode_liveprovebench.txt
+base_branch: main
+
+runner:
+  cwd: /mnt/nvme1/jacky/workspace/_eval_lb/numina-lean-agent
+  task_type: folder
+  max_rounds: 5
+  permission_mode: bypassPermissions
+  # Paths are relative to runner.cwd (numina-lean-agent/).
+  # Everything lives under experiments/, which is already in .gitignore.
+  result_dir: experiments/liveprovebench/results
+  mcp_log_dir: experiments/liveprovebench/mcp_logs
+  tmp_prompt_dir: experiments/liveprovebench/tmp_prompts
+  # Pause between problems to avoid hitting rate / quota limits.
+  # CLI flag --sleep-between overrides this. Set to 0 to disable.
+  sleep_between_tasks_minutes: 0
+
+# After `git checkout`, rebuild the Lean project so the freshly-checked-out
+# branch is in a compilable state before the agent runs. Set enabled: false
+# to skip (e.g. if you've already built manually).
+lake_build:
+  enabled: true
+  cmd: ["lake", "build", "LiveProveBench"]
+  timeout_seconds: 1800
+
+git:
+  skip_if_branch_exists: true
+  commit_after: true
+  commit_message_template: "run {nn}_{name}"

config/lists.txt

@@ -0,0 +1,22 @@
+# ProblemName                        LeanFolder                                                     Blueprint
+# Paths relative to this file's directory (/mnt/nvme1/jacky/workspace/_eval_lb).
+PicardGroupUfd                       LiveProveBench/LiveProveBench/PicardGroupUfd                   LiveProveBench/blueprint/src/theorems/picard-group-ufd.tex
+CondorcetJury                        LiveProveBench/LiveProveBench/CondorcetJury                    LiveProveBench/blueprint/src/theorems/condorcet-jury.tex
+Worpitzky                            LiveProveBench/LiveProveBench/Worpitzky                        LiveProveBench/blueprint/src/theorems/worpitzky.tex
+Dilworth                             LiveProveBench/LiveProveBench/Dilworth                         LiveProveBench/blueprint/src/theorems/dilworth.tex
+PolygonalNumberTheorem               LiveProveBench/LiveProveBench/PolygonalNumberTheorem           LiveProveBench/blueprint/src/theorems/polygonal-number-theorem.tex
+SinkhornTheorem                      LiveProveBench/LiveProveBench/SinkhornTheorem                  LiveProveBench/blueprint/src/theorems/sinkhorn-theorem.tex
+SchurRamsey                          LiveProveBench/LiveProveBench/SchurRamsey                      LiveProveBench/blueprint/src/theorems/schur-ramsey.tex
+RiemannSeries                        LiveProveBench/LiveProveBench/RiemannSeries                    LiveProveBench/blueprint/src/theorems/riemann-series.tex
+VonStaudtClausen                     LiveProveBench/LiveProveBench/VonStaudtClausen                 LiveProveBench/blueprint/src/theorems/von-staudt-clausen.tex
+AndersonTheorem                      LiveProveBench/LiveProveBench/AndersonTheorem                  LiveProveBench/blueprint/src/theorems/anderson-theorem.tex
+BanachMazur                          LiveProveBench/LiveProveBench/BanachMazur                      LiveProveBench/blueprint/src/theorems/banach-mazur.tex
+BrascampLieb                         LiveProveBench/LiveProveBench/BrascampLieb                     LiveProveBench/blueprint/src/theorems/brascamp-lieb.tex
+MertensFirstTheorem                  LiveProveBench/LiveProveBench/MertensFirstTheorem              LiveProveBench/blueprint/src/theorems/mertens-first-theorem.tex
+PicardTheorem                        LiveProveBench/LiveProveBench/PicardTheorem                    LiveProveBench/blueprint/src/theorems/picard-theorem.tex
+BorsukUlamTheorem                    LiveProveBench/LiveProveBench/BorsukUlamTheorem                LiveProveBench/blueprint/src/theorems/borsuk-ulam-theorem.tex
+FareySequence                        LiveProveBench/LiveProveBench/FareySequence                    LiveProveBench/blueprint/src/theorems/farey-sequence.tex
+ErdosGallaiTheorem                   LiveProveBench/LiveProveBench/ErdosGallaiTheorem               LiveProveBench/blueprint/src/theorems/erdos-gallai-theorem.tex
+DillerDressTheorem                   LiveProveBench/LiveProveBench/DillerDressTheorem               LiveProveBench/blueprint/src/theorems/diller-dress-theorem.tex
+DefinabilityNaturalsInRationals      LiveProveBench/LiveProveBench/DefinabilityNaturalsInRationals  LiveProveBench/blueprint/src/theorems/definability-naturals-in-rationals.tex
+KaplanskyTheoremOnQuadraticForms     LiveProveBench/LiveProveBench/KaplanskyTheoremOnQuadraticForms LiveProveBench/blueprint/src/theorems/kaplansky-theorem-on-quadratic-forms.tex

prompts/BLUEPRINT_template.md

@@ -0,0 +1,73 @@
+# Project Blueprint
+
+> Single source of truth for this theorem's progress. Update IMMEDIATELY after
+> any lemma status change. Do not batch updates.
+
+## Progress Summary
+- **Total items**: <N>
+- **Status**: done: <a> | partial: <b> | todo: <c>
+
+Status legend (from `prompts/docs/prompts/common.md`):
+- `done`     — completely proven, no sorry, compiles
+- `partial`  — partially proven, still has sorry
+- `todo`     — not started
+
+---
+
+# lemma lem:<label>
+
+## meta
+- **label**: `lem:<label>`                    <!-- same as the blueprint .tex `\label{lem:...}` -->
+- **lean**: `<Namespace.declaration>`         <!-- same as the blueprint .tex `\lean{...}` -->
+- **uses**: [[lem:<other1>], [lem:<other2>]]  <!-- dependency list; mirror the .tex `\uses{...}` -->
+- **file**: `LiveProveBench/<Problem>/<File>.lean:<line>`
+- **status**: `todo` | `partial` | `done`
+- **attempts**: `<current> / <budget>`
+
+## statement
+<Informal statement, copied/paraphrased from the blueprint .tex.>
+
+## proof
+<Informal proof, detailed enough to formalize step-by-step.
+ If still thinking, leave a stub and return after consulting Gemini
+ (`skills/cli/informal_prover.py`) or the Blueprint Agent workflow
+ in `prompts/docs/prompts/blueprint_agent.md`.>
+
+---
+
+# theorem thm:<main>
+
+## meta
+- **label**: `thm:<main>`
+- **lean**: `<Namespace.main_theorem>`
+- **uses**: [[lem:<sub1>], [lem:<sub2>]]
+- **file**: `LiveProveBench/<Problem>/MainTheorem.lean:<line>`
+- **status**: `todo` | `partial` | `done`
+- **attempts**: `<current> / <budget>`
+
+## statement
+<Main theorem statement.>
+
+## proof
+<Informal proof: how the sub-lemmas compose into the main theorem.>
+
+---
+
+## Notes
+
+- Each `lemma` / `theorem` / `definition` in the `.tex` blueprint should have
+  one entry here, in dependency order (leaves first, main theorem last).
+- Keep `meta.file` pointing at the actual Lean declaration (use `file:line`).
+- When a lemma becomes `done`, also add a status comment in the Lean source:
+
+  ```lean
+  /- (by claude)
+  State: done
+  Priority: <1-5>
+  Attempts: <N> / <M>
+  tmp file: <path_or_empty>
+  -/
+  lemma name : statement := by ...
+  ```
+
+  (Format from `prompts/docs/prompts/common.md` §3.)

prompts/prompt_hard_mode_liveprovebench.txt

@@ -0,0 +1,85 @@
+**FIRST ACTION**: Read the skill overviews now — `skills/search/SKILL.md`, `skills/verification/SKILL.md`, `skills/llm/SKILL.md`, `skills/code-transform/SKILL.md`, `skills/sorrifier/SKILL.md`. For any tool's exact CLI invocation, read the corresponding `reference-<tool>.md` in that directory.
+
+You are Lean Coordinator.
+
+## MUST READ FIRST
+(Paths are relative to cwd `numina-lean-agent/`; docs live under `prompts/docs/prompts/`.)
+1. prompts/docs/prompts/common.md (shared rules)
+2. prompts/docs/prompts/coordinator.md (your workflow)
+3. prompts/docs/prompts/blueprint_agent.md (blueprint creation and refinement)
+4. prompts/docs/prompts/proof_agent.md (proof strategies)
+5. prompts/docs/prompts/sketch_agent.md (formalization)
+6. GPT_HINT.md (hints for the proof, if available)
+
+## Key Rules (see docs for details)
+- ALL work must go through Task tool subagent. You are forbidden from doing work directly.
+- Use `python skills/cli/lean_check.py FILE` for verification (NOT `lake build`)
+- Use `python skills/cli/informal_prover.py` when informal proof is insufficient
+- Use `python skills/cli/discussion_partner.py` for strategic advice from Gemini
+- Mathlib not having it is NOT an excuse to give up - build it yourself step by step
+- Use emoji for status: done, partial, todo
+- Tmp file: First add comment in original file, THEN create tmp file in `tmp/` subfolder alongside original (NEVER in /tmp)
+- Don't use axiom. Use sorry for unproven statements.
+- DO NOT say 'Mathlib lacks in some infrastructure'. You are powerful, you can create a new file and implement the missing infrastructure.
+- DO NOT do enumerate when there are infinite possibilities. You should think critically and creatively or discuss with Gemini to find a general solution.
+
+## Workflow
+1. Read target file to understand current state
+2. For each lemma needing work:
+   - If informal proof unclear → Sketch Agent (use `python skills/cli/informal_prover.py`)
+   - If formalized but unproven → Proof Agent
+   - If too complex/stuck → Blueprint Agent (split into sub-lemmas)
+   - If proof broken and needs isolation → use **sorrifier** workflow (`skills/sorrifier/SKILL.md`)
+3. Update BLUEPRINT immediately after progress
+
+## HINT
+There is a hint for the proof in the GPT_HINT_v1.md file. Please read it carefully. You can mention it in your prompt for subagents.
+
+## Blueprint (authoritative informal proof)
+
+Read the blueprint file at:
+
+  __BLUEPRINT_PATH__
+
+It is the authoritative informal proof for this theorem. Use it to guide the
+formal proof: each `\label{lem:...}` entry corresponds to a Lean lemma name
+given by `\lean{...}`, and the `\uses{...}` lines define the dependency graph
+between lemmas. Do not change the statements of theorems or lemmas.
+
+## Target
+
+The target folder is:
+
+  __TARGET_FOLDER__
+
+It contains `MainTheorem.lean` (the goal; statements must remain unchanged)
+and `BackgroundLemmas.lean` (helpers, currently with `sorry` placeholders).
+Prove every `sorry` and make the folder compile cleanly.
+
+## Progress tracker (BLUEPRINT.md)
+
+Maintain a `BLUEPRINT.md` file **inside the target folder above**
+(`__TARGET_FOLDER__/BLUEPRINT.md`) as the single-source-of-truth progress
+tracker. If it does not exist, **copy the template from
+`prompts/BLUEPRINT_template.md`** and fill it in using the `.tex` blueprint:
+one entry per `\label{lem:...}` / `\label{thm:...}`, in dependency order,
+with `lean:` / `file:` / `uses:` / `status:` / `attempts:` populated.
+Update it immediately after any lemma status change — do not rely on the
+session-scoped TodoWrite for this.
+
+## Session End (CRITICAL FORMAT)
+
+**Your response MUST end with exactly this line (no markdown, no extra text):**
+
+```
+END_REASON:COMPLETE
+```
+or
+```
+END_REASON:LIMIT
+```
+
+- `COMPLETE`: Main theorem proven successfully
+- `LIMIT`: Made progress but can't complete in this session
+
+This line must be the LAST line of your response. No text after it.