[codex] Pin Lean managed workspace baseline

AGENTS.md

@@ -19,8 +19,9 @@ Core rules:
 - Formalization/proof readiness should inspect local Lean readiness first; inspect Numina/backend readiness only when the user asks for an optional Lean-specialist backend.
 - Setup-only readiness should focus on local Lean/mathlib state, and should mention or inspect Numina only when the user asks for the optional official backend.
 - Do not require API keys for the default coding-agent path.
-- Shared workspace is the default Lean project context; Numina may target it instead of upstream examples.
-- Prefer the user's existing Lake project. Use the shared `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` only when a standalone file needs project context.
+- Shared workspace is the default Lean project context for standalone work; Numina may target it instead of upstream examples.
+- Prefer the user's existing Lake project. Use the shared `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` only when a standalone file needs project context, and default that managed workspace to `leanprover/lean4:v4.28.0` unless the user explicitly overrides it.
+- Use `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/<version-key>/` for standalone tasks that need a different Lean/mathlib revision; do not overwrite the canonical managed workspace for version drift.
 - Preserve theorem statements unless the user explicitly approves a change.
 - Reject final patches containing `sorry`, `admit`, or newly introduced `axiom`.
 - Do not commit API keys, local runtime state, or machine-specific Numina paths.

README.md

@@ -66,6 +66,20 @@ For formalization or proof repair, start with:
 skills/lean-formalization/SKILL.md
 ```
 
+## Supported Scope
+
+- Lean project/workspace inspection.
+- Reusable shared `~/.ai4math/lean-workspace` setup for standalone Lean files, using the AI4Math managed baseline `leanprover/lean4:v4.28.0` unless explicitly overridden.
+- Theorem formalization, proof repair, proof completion, and `sorry` completion.
+- Patch review for `sorry`, `admit`, newly introduced `axiom`, and theorem statement drift.
+- Minimal failing Lean fragment extraction when a proof is blocked.
+- Related-work-informed Lean-specialist patterns: theorem-state loops, premise retrieval, bounded proof search, failure memory, validation oracles, and minimal handoff.
+- Optional Lean-specialist backend adapter flow, currently implemented for official `project-numina/numina-lean-agent` deployment/calls mediated by the coding agent.
+
+Numina is optional and is the only built-in deployable backend adapter. The public CLI does not expose a parallel `numina-*` workflow; `doctor` reports readiness and `configure --setup-numina --project-name <name>` performs the reviewed local setup under `~/.ai4math/numina-runtime/` by default.
+
+Future backend adapters can follow `skills/lean-runtime/references/backend_adapter_checklist.md`, but should not be described as supported until deployment, readiness checks, invocation, validation, and failure triage are documented.
+
 ## Repository Layout
 
 ```text

README.zh-CN.md

@@ -52,6 +52,23 @@ skills/lean-setup/SKILL.md
 skills/lean-formalization/SKILL.md
 ```
 
+`approve` 表示执行下一步，`revise` 表示先修改计划，`reject` 表示停止当前路线，
+`skip` 表示跳过当前阶段。修改 theorem statement、设置 Numina、编辑源码和接受最终 proof
+claim 前都应先请求用户确认。
+
+## 支持范围
+
+- Lean project/workspace inspection。
+- 只配置环境时，可创建或复用共享 `~/.ai4math/lean-workspace`；默认使用 AI4Math managed baseline `leanprover/lean4:v4.28.0`，除非用户明确覆盖。
+- theorem formalization、proof repair、proof completion 和 `sorry` completion。
+- patch review：检查 `sorry`、`admit`、新引入的 `axiom` 和 theorem statement drift。
+- 可选 Lean 专用 agent backend adapter 流程；当前实现的是由 coding agent 协调的 official `project-numina/numina-lean-agent` runtime 设置和调用。
+- proof blocked 时抽取最小失败 Lean fragment。
+- 借鉴 Lean 专用 agent 模式：theorem-state loop、premise retrieval、bounded proof search、失败记忆、validation oracle 和 minimal handoff。
+
+Numina 是可选链路，也是当前唯一内置可部署 backend adapter。公共 CLI 不提供并行的 `numina-*` workflow；`doctor` 用于报告 readiness，`configure --setup-numina --project-name <name>` 用于在 review 后执行本地设置，默认位置为 `~/.ai4math/numina-runtime/`。只有当用户明确要求 `Numina`、`official Lean Agent`、批量 proof search 或外部 subagent run 时，才应进入 official Numina backend。
+
+未来 backend adapter 可参考 `skills/lean-runtime/references/backend_adapter_checklist.md`，但在 deployment、readiness checks、调用、validation 和 failure triage 文档化前，不要写成已支持。
 ## 仓库结构
 
 ```text

skills/lean-runtime/config/lean_agent.example.toml

@@ -9,7 +9,7 @@ managed_workspace_template = "math"
 reuse_managed_workspace = true
 workspace_key = "lean-toolchain"
 align_workspace_versions = true
-preferred_toolchain = "auto"
+preferred_toolchain = "leanprover/lean4:v4.28.0"
 preferred_mathlib_rev = "auto"
 allow_user_project_version_changes = false
 

skills/lean-runtime/references/direct_lean_workflow.md

@@ -33,7 +33,7 @@ Do not route creative proof search through helper commands. `prove`, `formalize`
 
 Prefer a user's existing Lake project when the target file is inside one. For standalone `.lean` files, use the reusable `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` so Lean, Lake, and mathlib artifacts are shared across tasks and projects.
 
-When a user project has its own `lean-toolchain` and mathlib revision, keep those versions unless the user explicitly approves a change. When creating a managed workspace, use the configured preferred toolchain or `auto`.
+When a user project has its own `lean-toolchain` and mathlib revision, keep those versions unless the user explicitly approves a change. When creating a managed workspace, default to the AI4Math canonical toolchain `leanprover/lean4:v4.28.0` unless the user explicitly overrides it; use a versioned workspace for other standalone revisions instead of overwriting the canonical workspace.
 
 ## Good Stopping Points
 

skills/lean-runtime/references/lean_runtime_configuration.md

@@ -28,22 +28,22 @@ Required default workflow tools are `git`, `python3`, `elan`, `lean`, and `lake`
 
 ## Reusable Lean Workspace
 
-For standalone tasks, prefer `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. Create it once with:
+For standalone tasks, prefer `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. This canonical managed workspace defaults to the AI4Math baseline toolchain `leanprover/lean4:v4.28.0`; use `--toolchain` only as an explicit override. Create it once with:
 
 ```bash
-python skills/lean-runtime/scripts/ai4m_lean.py configure --cwd . --create-workspace --toolchain leanprover/lean4:v4.28.0
+python skills/lean-runtime/scripts/ai4m_lean.py configure --cwd . --create-workspace
 ```
 
 Equivalent Lake commands:
 
 ```bash
-lake new lean_workspace math
-lake update
-lake exe cache get
-lake build
+elan run leanprover/lean4:v4.28.0 lake new lean_workspace math
+elan run leanprover/lean4:v4.28.0 lake update
+elan run leanprover/lean4:v4.28.0 lake exe cache get
+elan run leanprover/lean4:v4.28.0 lake build
 ```
 
-If a user project already has `lean-toolchain` and `lakefile.{lean,toml}`, use that project and do not change versions without approval. If a standalone task needs a different Lean/mathlib revision than the shared managed workspace, use a versioned workspace under `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/`.
+If a user project already has `lean-toolchain` and `lakefile.{lean,toml}`, use that project and do not change versions without approval. If the canonical workspace already has `lake-manifest.json` and `.lake/`, reuse it instead of rerunning cache/build. If a standalone task needs a different Lean/mathlib revision than the shared managed workspace, use a versioned workspace under `${AI4MATH_HOME:-~/.ai4math}/lean-workspaces/` instead of overwriting `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`.
 
 ## Local Config
 
@@ -54,7 +54,7 @@ Machine-specific settings live in `.ai4math/lean_agent.local.toml` and should no
 workspace_mode = "reuse-managed"
 managed_workspace_path = "~/.ai4math/lean-workspace"
 align_workspace_versions = true
-preferred_toolchain = "auto"
+preferred_toolchain = "leanprover/lean4:v4.28.0"
 
 [agent]
 mode = "coding-agent"

skills/lean-runtime/scripts/ai4m_lean.py

@@ -77,7 +77,7 @@ def build_parser() -> argparse.ArgumentParser:
     add_common(configure_parser)
     configure_parser.add_argument("--target", default=None)
     configure_parser.add_argument("--create-workspace", action="store_true")
-    configure_parser.add_argument("--toolchain", default=None, help="Optional Lean toolchain for managed workspace")
+    configure_parser.add_argument("--toolchain", default=None, help="Override the default AI4Math managed workspace toolchain")
     configure_parser.add_argument("--save-local", action="store_true")
     configure_parser.add_argument("--dry-run", action="store_true")
     configure_parser.add_argument("--setup-numina", action="store_true", help="Install/configure official Numina runtime after review")

skills/lean-runtime/scripts/common.py

@@ -21,6 +21,7 @@
 SKILL_ROOT = Path(__file__).resolve().parents[1]
 DEFAULT_CONFIG = SKILL_ROOT / "config" / "lean_agent.example.toml"
 ENV_KEY_RE = re.compile(r"^[A-Za-z_][A-Za-z0-9_]*$")
+CANONICAL_LEAN_TOOLCHAIN = "leanprover/lean4:v4.28.0"
 
 
 def deep_merge(base: dict[str, Any], overlay: dict[str, Any]) -> dict[str, Any]:

skills/lean-runtime/scripts/configure_lean.py

@@ -5,7 +5,7 @@
 from typing import Any
 
 from check_lean_project import find_project_root, read_mathlib_revision, read_toolchain
-from common import ai4math_home, ensure_ai4math_gitignore, expand_path, read_config, run_command, update_local_toml
+from common import CANONICAL_LEAN_TOOLCHAIN, ai4math_home, ensure_ai4math_gitignore, expand_path, read_config, run_command, update_local_toml
 from numina_runtime import execute_configure_plan, numina_readiness
 from tool_status import find_tool
 
@@ -36,6 +36,19 @@ def _workspace_setup_commands(lake: str, toolchain: str | None, workspace: Path)
     return commands
 
 
+def _effective_managed_toolchain(config: dict[str, Any], requested_toolchain: str | None) -> str:
+    if requested_toolchain is not None:
+        return requested_toolchain.strip() or CANONICAL_LEAN_TOOLCHAIN
+    configured = str(config.get("lean", {}).get("preferred_toolchain") or "").strip()
+    if configured and configured != "auto":
+        return configured
+    return CANONICAL_LEAN_TOOLCHAIN
+
+
+def _workspace_needs_setup(workspace: Path) -> bool:
+    return not ((workspace / "lake-manifest.json").exists() and (workspace / ".lake").exists())
+
+
 def _action_failed(action: dict[str, Any]) -> bool:
     return not action.get("skipped") and not action.get("recoverable") and not action.get("ok", False)
 
@@ -113,6 +126,7 @@ def configure(
 
     config = read_config(cwd_path, config_path)
     lean = config.get("lean", {})
+    effective_toolchain = _effective_managed_toolchain(config, toolchain)
     workspace = expand_path(lean.get("managed_workspace_path"), cwd_path) or (ai4math_home(cwd_path) / "lean-workspace")
     workspace_root_config = expand_path(lean.get("managed_workspace_root"), cwd_path) or (workspace.parent / "lean-workspaces")
     workspace_actions: list[dict[str, Any]] = []
@@ -123,14 +137,14 @@ def configure(
         created_path = parent / lake_project_name
         if dry_run:
             workspace_actions.append({
-                "command": _lake_command(lake, toolchain, ["new", lake_project_name, "math"]),
+                "command": _lake_command(lake, effective_toolchain, ["new", lake_project_name, "math"]),
                 "cwd": str(parent),
                 "skipped": True,
                 "reason": "dry_run",
             })
         elif not workspace.exists():
             parent.mkdir(parents=True, exist_ok=True)
-            created = run_command(_lake_command(lake, toolchain, ["new", lake_project_name, "math"]), cwd=parent)
+            created = run_command(_lake_command(lake, effective_toolchain, ["new", lake_project_name, "math"]), cwd=parent)
             if not created.get("ok") and find_project_root(created_path):
                 created["recoverable"] = True
                 created["recovered_by"] = "lake_project_files_created"
@@ -153,8 +167,8 @@ def configure(
                 "stdout": "",
                 "stderr": "",
             })
-        if not dry_run and find_project_root(workspace):
-            for command in _workspace_setup_commands(lake, toolchain, workspace):
+        if not dry_run and find_project_root(workspace) and _workspace_needs_setup(workspace):
+            for command in _workspace_setup_commands(lake, effective_toolchain, workspace):
                 workspace_actions.append(run_command(command, cwd=workspace, timeout=1800))
 
     workspace_info = _workspace_info(workspace)
@@ -170,7 +184,7 @@ def configure(
                 "reuse_managed_workspace": True,
                 "workspace_key": "lean-toolchain",
                 "align_workspace_versions": True,
-                "preferred_toolchain": toolchain or "auto",
+                "preferred_toolchain": effective_toolchain,
                 "preferred_mathlib_rev": "auto",
                 "allow_user_project_version_changes": False,
             },

skills/lean-runtime/scripts/verify_delivery.py

@@ -253,6 +253,11 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]:
         "When creating an isolated test directory or workspace",
         "suggest a safe default name",
         "use the default if the user has no naming preference",
+        "canonical managed workspace",
+        "AI4Math managed baseline toolchain `leanprover/lean4:v4.28.0`",
+        "reuse it instead of rebuilding or downloading again",
+        "Do not overwrite the canonical managed workspace",
+        "lean-workspaces/<version-key>/",
         "After successful setup or smoke-test validation",
         "Offer a short next-step menu",
         "inspect an existing Lean/Lake project",
@@ -268,6 +273,10 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]:
     repo_root_command_hits = [phrase for phrase in repo_root_commands if phrase in text]
     openai_required = [
         "不要向用户索要 theorem target",
+        "已有 Lake 项目优先沿用项目自己的 lean-toolchain 和 lake-manifest",
+        "standalone 任务默认复用 ~/.ai4math/lean-workspace",
+        "AI4Math managed baseline leanprover/lean4:v4.28.0",
+        "避免重复下载和路径分裂",
         "setup 完成后主动给出下一步菜单",
         "所有实现应复用 lean-runtime",
         "默认 Lean/mathlib 环境配置不需要 API key",

skills/lean-runtime/tests/test_cli.py

@@ -13,6 +13,7 @@
 sys.path.insert(0, str(SKILL_ROOT / "scripts"))
 
 from ai4m_lean import EXIT_LEAN_FAILED, _exit_code  # noqa: E402
+from common import CANONICAL_LEAN_TOOLCHAIN  # noqa: E402
 from verify_delivery import _lean_setup_entrypoint_check, _package_hygiene, _root_discovery_boundary_check  # noqa: E402
 
 CLI = SKILL_ROOT / "scripts" / "ai4m_lean.py"
@@ -131,6 +132,34 @@ def test_configure_setup_numina_dry_run_outputs_official_upstream(self) -> None:
         self.assertIn("https://github.com/project-numina/numina-lean-agent", str(commands))
         self.assertIn(["./setup.sh", "demo_project"], commands)
 
+    def test_configure_create_workspace_dry_run_defaults_to_canonical_toolchain(self) -> None:
+        with tempfile.TemporaryDirectory() as tmp:
+            root = Path(tmp)
+            result = subprocess.run(
+                [
+                    sys.executable,
+                    str(CLI),
+                    "configure",
+                    "--cwd",
+                    str(root),
+                    "--create-workspace",
+                    "--dry-run",
+                ],
+                text=True,
+                capture_output=True,
+                check=False,
+                env={
+                    **os.environ,
+                    "AI4MATH_HOME": str(root / "shared-ai4math"),
+                    "AI4MATH_LEAN_WORKSPACE": "",
+                    "AI4MATH_LEAN_TOOLCHAIN": "",
+                },
+            )
+        self.assertIn(result.returncode, {0, 4}, result.stderr)
+        payload = json.loads(result.stdout)
+        command = payload["workspace_actions"][0]["command"]
+        self.assertEqual(command[1:4], ["run", CANONICAL_LEAN_TOOLCHAIN, "lake"])
+
     def test_lean_workspace_deploy_failure_uses_lean_exit_code(self) -> None:
         self.assertEqual(
             _exit_code({"ok": False, "status": "lean_workspace_setup_failed"}),

skills/lean-runtime/tests/test_common_config.py

@@ -9,7 +9,7 @@
 SCRIPTS = Path(__file__).resolve().parents[1] / "scripts"
 sys.path.insert(0, str(SCRIPTS))
 
-from common import ai4math_home, expand_path, load_toml, read_env_local, write_env_local  # noqa: E402
+from common import CANONICAL_LEAN_TOOLCHAIN, ai4math_home, expand_path, load_toml, read_config, read_env_local, write_env_local  # noqa: E402
 
 
 class CommonConfigTests(unittest.TestCase):
@@ -47,6 +47,25 @@ def test_ai4math_home_honors_environment_override(self) -> None:
 
             self.assertEqual(result, custom)
 
+    def test_default_config_uses_canonical_toolchain(self) -> None:
+        with tempfile.TemporaryDirectory() as tmp:
+            root = Path(tmp)
+
+            with patch.dict("os.environ", {"AI4MATH_LEAN_TOOLCHAIN": ""}, clear=False):
+                config = read_config(root)
+
+            self.assertEqual(config["lean"]["preferred_toolchain"], CANONICAL_LEAN_TOOLCHAIN)
+
+    def test_environment_can_override_canonical_toolchain(self) -> None:
+        with tempfile.TemporaryDirectory() as tmp:
+            root = Path(tmp)
+            override = "leanprover/lean4:v4.26.0"
+
+            with patch.dict("os.environ", {"AI4MATH_LEAN_TOOLCHAIN": override}, clear=False):
+                config = read_config(root)
+
+            self.assertEqual(config["lean"]["preferred_toolchain"], override)
+
     def test_write_env_local_updates_values_and_is_ignored(self) -> None:
         with tempfile.TemporaryDirectory() as tmp:
             root = Path(tmp)