From 3649a6b6d86374c8ce701b8121dd7befe4f0a015 Mon Sep 17 00:00:00 2001 From: hehepig166 <1260647889@qq.com> Date: Thu, 16 Apr 2026 17:20:11 +0000 Subject: [PATCH 1/2] Add LiveProveBench runner driver Sequential driver that, for each problem listed in config/lists.txt, checks out the LiveProveBench main branch, creates (or reuses) an NN_ branch, rebuilds via `lake build LiveProveBench`, runs the hard-mode prompt extended to reference the matching blueprint .tex path (not inlined), and commits the result on the problem branch. Supports --from (by index or name), --count, --only/--skip, --sleep-between, and --dry-run. All outputs land under experiments/liveprovebench/ (already gitignored). Co-Authored-By: Claude Opus 4.7 (1M context) --- config/config_liveprovebench.yaml | 46 +++ config/lists.txt | 22 ++ prompts/prompt_hard_mode_liveprovebench.txt | 73 ++++ scripts/run_liveprovebench.py | 351 ++++++++++++++++++++ 4 files changed, 492 insertions(+) create mode 100644 config/config_liveprovebench.yaml create mode 100644 config/lists.txt create mode 100644 prompts/prompt_hard_mode_liveprovebench.txt create mode 100644 scripts/run_liveprovebench.py diff --git a/config/config_liveprovebench.yaml b/config/config_liveprovebench.yaml new file mode 100644 index 0000000..5af55a5 --- /dev/null +++ b/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}" \ No newline at end of file diff --git a/config/lists.txt b/config/lists.txt new file mode 100644 index 0000000..145bc89 --- /dev/null +++ b/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 diff --git a/prompts/prompt_hard_mode_liveprovebench.txt b/prompts/prompt_hard_mode_liveprovebench.txt new file mode 100644 index 0000000..2c4f465 --- /dev/null +++ b/prompts/prompt_hard_mode_liveprovebench.txt @@ -0,0 +1,73 @@ +**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-.md` in that directory. + +You are Lean Coordinator. + +## MUST READ FIRST +1. docs/prompts/common.md (shared rules) +2. docs/prompts/coordinator.md (your workflow) +3. docs/prompts/blueprint_agent.md (blueprint creation and refinement) +4. docs/prompts/proof_agent.md (proof strategies) +5. 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. + +## 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. diff --git a/scripts/run_liveprovebench.py b/scripts/run_liveprovebench.py new file mode 100644 index 0000000..1d12140 --- /dev/null +++ b/scripts/run_liveprovebench.py @@ -0,0 +1,351 @@ +#!/usr/bin/env python3 +""" +Driver for running the Numina Lean Agent across LiveProveBench problems. + +Reads problem rows from lists.txt (ProblemName / LeanFolder / Blueprint, all +relative to lists_base) and shared settings from a YAML config. For each row: + + 1. In the LiveProveBench repo: `git checkout main`, then create or reuse a + branch `NN_` (NN = 1-based zero-padded index from lists.txt). + 2. Build the per-problem prompt by substituting absolute blueprint and + target-folder paths into the prompt template. The blueprint content is + NOT inlined — only its path is given to the agent. + 3. Run the numina-lean-agent runner on the target folder. + 4. Optionally `git add -A && git commit` the produced changes on that branch. + +Usage: + python scripts/run_liveprovebench.py [--config config/config_liveprovebench.yaml] + [--only NAME] [--skip NAME]... + [--from N] [--dry-run] +""" + +import argparse +import csv +import subprocess +import sys +import time +from datetime import datetime +from pathlib import Path +from typing import List, Optional, Tuple + +import yaml + +# Make sibling modules importable when run as `python scripts/run_liveprovebench.py` +SCRIPT_DIR = Path(__file__).resolve().parent +REPO_ROOT = SCRIPT_DIR.parent +if str(REPO_ROOT) not in sys.path: + sys.path.insert(0, str(REPO_ROOT)) + +from scripts.task import TaskMetadata, TaskResult +from scripts.runner import run_task + + +def parse_lists(lists_file: Path, lists_base: Path) -> List[Tuple[str, Path, Path]]: + """Parse the 3-column lists.txt. Returns [(name, lean_folder_abs, blueprint_abs), ...].""" + rows: List[Tuple[str, Path, Path]] = [] + for lineno, raw in enumerate(lists_file.read_text(encoding="utf-8").splitlines(), 1): + line = raw.strip() + if not line or line.startswith("#"): + continue + parts = line.split() + if len(parts) != 3: + raise ValueError( + f"{lists_file}:{lineno}: expected 3 whitespace-separated columns, got {len(parts)}: {line!r}" + ) + name, lean_rel, blueprint_rel = parts + lean_abs = (lists_base / lean_rel).resolve() + blueprint_abs = (lists_base / blueprint_rel).resolve() + if not lean_abs.is_dir(): + raise FileNotFoundError(f"{lists_file}:{lineno}: lean folder not found: {lean_abs}") + if not blueprint_abs.is_file(): + raise FileNotFoundError(f"{lists_file}:{lineno}: blueprint not found: {blueprint_abs}") + rows.append((name, lean_abs, blueprint_abs)) + return rows + + +def run_git(args: List[str], cwd: Path, dry_run: bool, check: bool = True) -> subprocess.CompletedProcess: + """Run a git command in cwd. Print it; skip execution in dry-run.""" + print(f"[git] ({cwd}) git {' '.join(args)}") + if dry_run: + return subprocess.CompletedProcess(args=args, returncode=0, stdout="", stderr="") + return subprocess.run( + ["git", *args], + cwd=str(cwd), + check=check, + text=True, + capture_output=True, + ) + + +def branch_exists(lean_repo: Path, branch: str) -> bool: + res = subprocess.run( + ["git", "rev-parse", "--verify", "--quiet", f"refs/heads/{branch}"], + cwd=str(lean_repo), + capture_output=True, + text=True, + ) + return res.returncode == 0 + + +def has_staged_or_unstaged_changes(lean_repo: Path) -> bool: + res = subprocess.run( + ["git", "status", "--porcelain"], + cwd=str(lean_repo), + capture_output=True, + text=True, + check=True, + ) + return bool(res.stdout.strip()) + + +def build_prompt(template: str, blueprint_abs: Path, target_folder_abs: Path) -> str: + return ( + template + .replace("__BLUEPRINT_PATH__", str(blueprint_abs)) + .replace("__TARGET_FOLDER__", str(target_folder_abs)) + ) + + +def resolve_runner_path(runner_cfg: dict, key: str) -> Path: + """Resolve a runner path relative to runner.cwd if not already absolute.""" + raw = Path(runner_cfg[key]) + if raw.is_absolute(): + return raw + return (Path(runner_cfg["cwd"]) / raw).resolve() + + +def append_summary(summary_path: Path, row: dict) -> None: + summary_path.parent.mkdir(parents=True, exist_ok=True) + header = ["timestamp", "nn", "name", "end_reason", "success", "rounds", "duration_s", "cost_usd", "branch"] + write_header = not summary_path.exists() + with open(summary_path, "a", encoding="utf-8", newline="") as f: + w = csv.DictWriter(f, fieldnames=header) + if write_header: + w.writeheader() + w.writerow({k: row.get(k, "") for k in header}) + + +def process_row( + nn: str, + name: str, + lean_folder: Path, + blueprint: Path, + cfg: dict, + template_text: str, + dry_run: bool, +) -> Optional[TaskResult]: + lean_repo = Path(cfg["lean_repo"]) + base_branch = cfg.get("base_branch", "main") + runner_cfg = cfg["runner"] + git_cfg = cfg.get("git", {}) + branch = f"{nn}_{name}" + + print("=" * 72) + print(f"[{nn}] {name}") + print(f" lean_folder: {lean_folder}") + print(f" blueprint: {blueprint}") + print(f" branch: {branch}") + print("=" * 72) + + # 1. git: checkout main, then branch + run_git(["checkout", base_branch], lean_repo, dry_run) + if dry_run: + print(f"[git] (dry-run) would ensure branch {branch} exists and check it out") + else: + if branch_exists(lean_repo, branch): + if git_cfg.get("skip_if_branch_exists", True): + print(f"[info] branch {branch} already exists, checking out") + run_git(["checkout", branch], lean_repo, dry_run=False) + else: + raise RuntimeError(f"branch {branch} already exists and skip_if_branch_exists=false") + else: + run_git(["checkout", "-b", branch], lean_repo, dry_run=False) + + # 1b. lake build the freshly-checked-out branch + lake_cfg = cfg.get("lake_build", {}) or {} + if lake_cfg.get("enabled", False): + cmd = list(lake_cfg.get("cmd", ["lake", "build"])) + timeout = int(lake_cfg.get("timeout_seconds", 1800)) + print(f"[lake] ({lean_repo}) {' '.join(cmd)} (timeout {timeout}s)") + if not dry_run: + res = subprocess.run(cmd, cwd=str(lean_repo), timeout=timeout) + if res.returncode != 0: + raise RuntimeError(f"lake build failed on branch {branch} (rc={res.returncode})") + + # 2. Build prompt + tmp_prompt_dir = resolve_runner_path(runner_cfg, "tmp_prompt_dir") + tmp_prompt_dir.mkdir(parents=True, exist_ok=True) + prompt_path = tmp_prompt_dir / f"{branch}.txt" + prompt_text = build_prompt(template_text, blueprint, lean_folder) + prompt_path.write_text(prompt_text, encoding="utf-8") + print(f"[info] wrote prompt to {prompt_path} ({len(prompt_text)} chars)") + + # 3. Build and run task + result_dir = resolve_runner_path(runner_cfg, "result_dir") + mcp_log_dir = resolve_runner_path(runner_cfg, "mcp_log_dir") + + task = TaskMetadata( + task_type=runner_cfg.get("task_type", "folder"), + target_path=lean_folder, + prompt_file=prompt_path, + cwd=Path(runner_cfg["cwd"]), + max_rounds=int(runner_cfg.get("max_rounds", 10)), + permission_mode=runner_cfg.get("permission_mode", "bypassPermissions"), + result_dir=result_dir, + mcp_log_dir=mcp_log_dir, + mcp_log_name=branch, + ) + + if dry_run: + print(f"[dry-run] would run_task with:") + print(f" target_path = {task.target_path}") + print(f" prompt_file = {task.prompt_file}") + print(f" cwd = {task.cwd}") + print(f" max_rounds = {task.max_rounds}") + print(f" result_dir = {task.result_dir}") + print(f" mcp_log_dir = {task.mcp_log_dir}") + print(f" mcp_log_name = {task.mcp_log_name}") + return None + + result = run_task(task) + + # 4. Optional commit on the problem branch + if git_cfg.get("commit_after", True): + if has_staged_or_unstaged_changes(lean_repo): + msg = git_cfg.get("commit_message_template", "run {nn}_{name}").format(nn=nn, name=name) + run_git(["add", "-A"], lean_repo, dry_run=False) + run_git(["commit", "-m", msg], lean_repo, dry_run=False) + else: + print(f"[info] no changes to commit on {branch}") + + # 5. Append summary row + summary_path = result_dir / "summary.csv" + append_summary( + summary_path, + { + "timestamp": datetime.now().isoformat(timespec="seconds"), + "nn": nn, + "name": name, + "end_reason": result.end_reason or "", + "success": str(result.success), + "rounds": result.rounds_used, + "duration_s": f"{result.duration_seconds:.1f}", + "cost_usd": f"{result.total_cost_usd:.4f}", + "branch": branch, + }, + ) + + return result + + +def main() -> int: + ap = argparse.ArgumentParser(description="Run numina-lean-agent across LiveProveBench problems.") + ap.add_argument("--config", default=str(REPO_ROOT / "config" / "config_liveprovebench.yaml"), + help="Path to YAML config (default: config/config_liveprovebench.yaml)") + ap.add_argument("--only", action="append", default=[], help="Only run these problem names (repeatable)") + ap.add_argument("--skip", action="append", default=[], help="Skip these problem names (repeatable)") + ap.add_argument("--from", dest="from_", default=None, + help="Start at this row: either a 1-based index (e.g. 5) or a ProblemName (e.g. Dilworth). " + "Numbering continues from lists.txt so NN stays stable across resumes.") + ap.add_argument("--count", type=int, default=None, help="Run at most this many problems after --from") + ap.add_argument("--sleep-between", type=float, default=None, + help="Minutes to sleep between problems (overrides runner.sleep_between_tasks_minutes). " + "Useful to avoid hitting rate / quota limits. 0 disables.") + ap.add_argument("--dry-run", action="store_true", help="Print planned actions without executing") + args = ap.parse_args() + + cfg_path = Path(args.config).resolve() + cfg = yaml.safe_load(cfg_path.read_text(encoding="utf-8")) + + lists_file = Path(cfg["lists_file"]).resolve() + lists_base = Path(cfg["lists_base"]).resolve() + lean_repo = Path(cfg["lean_repo"]).resolve() + if not lean_repo.is_dir(): + print(f"[error] lean_repo not found: {lean_repo}", file=sys.stderr) + return 1 + + rows = parse_lists(lists_file, lists_base) + if not rows: + print(f"[error] no rows in {lists_file}", file=sys.stderr) + return 1 + + # Load prompt template once + template_path = Path(cfg["prompt_template"]) + if not template_path.is_absolute(): + template_path = Path(cfg["runner"]["cwd"]) / template_path + template_text = template_path.read_text(encoding="utf-8") + + only_set = set(args.only) + skip_set = set(args.skip) + + # Resolve --from: accept int or problem name + from_idx = 1 + if args.from_: + if args.from_.isdigit(): + from_idx = int(args.from_) + else: + name_to_idx = {n: i for i, (n, *_rest) in enumerate(rows, start=1)} + if args.from_ not in name_to_idx: + print(f"[error] --from {args.from_!r} not found in lists.txt", file=sys.stderr) + return 1 + from_idx = name_to_idx[args.from_] + print(f"[info] starting from row {from_idx} ({rows[from_idx - 1][0]})") + + # Resolve inter-task sleep (minutes → seconds) + sleep_minutes = args.sleep_between + if sleep_minutes is None: + sleep_minutes = float(cfg.get("runner", {}).get("sleep_between_tasks_minutes", 0) or 0) + sleep_seconds = max(0.0, sleep_minutes * 60.0) + + ran_count = 0 + results: List[Tuple[str, str, Optional[TaskResult]]] = [] + planned = [ + (idx, name, lf, bp) for idx, (name, lf, bp) in enumerate(rows, start=1) + if idx >= from_idx and (not only_set or name in only_set) and name not in skip_set + ] + if args.count is not None: + planned = planned[: args.count] + + for k, (idx, name, lean_folder, blueprint) in enumerate(planned): + nn = f"{idx:02d}" + try: + result = process_row(nn, name, lean_folder, blueprint, cfg, template_text, args.dry_run) + except subprocess.CalledProcessError as e: + print(f"[error] {nn} {name}: git command failed: {e}\n{e.stderr}", file=sys.stderr) + results.append((nn, name, None)) + result = None + except Exception as e: + print(f"[error] {nn} {name}: {e}", file=sys.stderr) + results.append((nn, name, None)) + result = None + else: + results.append((nn, name, result)) + ran_count += 1 + + # Sleep between problems (not after the last one) + if sleep_seconds > 0 and k < len(planned) - 1: + if args.dry_run: + print(f"[dry-run] would sleep {sleep_minutes:g} min before next problem") + else: + print(f"[info] sleeping {sleep_minutes:g} min before next problem...") + time.sleep(sleep_seconds) + + # Final summary + print("\n" + "=" * 72) + print("OVERALL SUMMARY") + print("=" * 72) + for nn, name, r in results: + if r is None: + status = "SKIPPED/ERROR" if not args.dry_run else "DRY-RUN" + else: + status = f"{r.end_reason or '-'} ({r.rounds_used} rounds, {r.duration_seconds:.0f}s)" + print(f" [{nn}] {name}: {status}") + + if args.dry_run: + return 0 + any_failed = any(r is None or not r.success for _, _, r in results) + return 1 if any_failed else 0 + + +if __name__ == "__main__": + sys.exit(main()) From 03636d56243c883102ef17425c63f27161418ece Mon Sep 17 00:00:00 2001 From: hehepig166 <1260647889@qq.com> Date: Fri, 17 Apr 2026 03:32:48 +0000 Subject: [PATCH 2/2] add blueprint template --- prompts/BLUEPRINT_template.md | 73 +++++++++++++++++++++ prompts/prompt_hard_mode_liveprovebench.txt | 22 +++++-- 2 files changed, 90 insertions(+), 5 deletions(-) create mode 100644 prompts/BLUEPRINT_template.md diff --git a/prompts/BLUEPRINT_template.md b/prompts/BLUEPRINT_template.md new file mode 100644 index 0000000..c437a7b --- /dev/null +++ b/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**: +- **Status**: done: | partial: | todo: + +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: