diff --git a/.agent.md b/.agent.md index cb5ad77..c4a8806 100644 --- a/.agent.md +++ b/.agent.md @@ -10,8 +10,10 @@ help the active agent find and load those Skill layers. - Skill entrypoints: - `skills/lean-setup/SKILL.md` - `skills/lean-formalization/SKILL.md` -- These skills are standalone. Do not require the user to clone - `AI4Math-Skill-Library` just to use them. +- Shared support layer: + - `skills/lean-runtime/` +- These public skills are standalone from `AI4Math-Skill-Library`, but both + entrypoints require the bundled `skills/lean-runtime/` support directory. ## Interactive Install Flow @@ -21,7 +23,8 @@ help the active agent find and load those Skill layers. 3. Inspect `AGENTS.md`, `SKILL.md`, and the declared Skill entrypoints before changing any configuration. 4. Detect the active coding-agent environment and its skill/config location. -5. Install or link the smallest directories that expose the intended `SKILL.md` files. +5. Install or link the smallest directories that expose the intended `SKILL.md` files, + plus the sibling `lean-runtime` support directory. Preserve existing configuration and do not overwrite unrelated files. 6. Do not write API keys, tokens, or private credentials into repository files. 7. Reload or restart the target agent only when its discovery mechanism requires diff --git a/.codex/INSTALL.md b/.codex/INSTALL.md index ee5ec3f..0b1b2f3 100644 --- a/.codex/INSTALL.md +++ b/.codex/INSTALL.md @@ -8,7 +8,8 @@ skills/lean-formalization/SKILL.md Use from the checkout by asking Codex to read `AGENTS.md`, `SKILL.md`, and the concrete Skill file. For local discovery, sync or link -`skills/lean-formalization/` into the Codex Skill path used by your -installation, then restart or reload if required. +`skills/lean-setup/` and `skills/lean-formalization/` into the Codex Skill path +used by your installation, and keep `skills/lean-runtime/` as their sibling +support directory. Then restart or reload if required. Do not duplicate workflow logic in `.codex/`; update the shared Skill layer. diff --git a/.cursor/rules/lean-formalization.mdc b/.cursor/rules/lean-formalization.mdc index 853cdb8..39f738b 100644 --- a/.cursor/rules/lean-formalization.mdc +++ b/.cursor/rules/lean-formalization.mdc @@ -9,6 +9,6 @@ alwaysApply: false Use `skills/lean-formalization/SKILL.md` as the canonical workflow. -This is a coding-agent-first Lean skill. The coding agent is the primary Lean worker: read/edit Lean, run Lean/Lake, iterate from errors, and validate final patches locally. Official Numina is an optional deployable subagent backend; preserve that deployment/call path but do not make it the default. Match the user's language by default; if the user's language is ambiguous, default to Chinese. Do not treat language switches as task resets. Lead the interaction: inspect context, summarize what is ready, recommend the next useful step, and ask at most one blocking question. When no target is provided, run or propose a safe local smoke/readiness check before asking for more input; use the bundled smoke test when no user target is available. Opening readiness should inspect local Lean readiness and Numina subagent readiness separately. 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. The helper CLI under `skills/lean-formalization/scripts/` is optional and should be used only for environment checks, structured validation, optional Numina readiness/setup, patch review, `sorry` detection, or minimal failure handoff. +This is a coding-agent-first Lean skill. The coding agent is the primary Lean worker: read/edit Lean, run Lean/Lake, iterate from errors, and validate final patches locally. Official Numina is the only currently supported deployable backend adapter; preserve that deployment/call path but do not make it the default. Archon and other backends are future adapters until their setup, call, credential, mutation, and validation contracts are documented. Match the user's language by default; if the user's language is ambiguous, default to Chinese. Do not treat language switches as task resets. Lead the interaction: inspect context, summarize what is ready, recommend the next useful step, and ask at most one blocking question. When no target is provided, run or propose a safe local smoke/readiness check before asking for more input; use the bundled smoke test when no user target is available. Opening readiness should inspect local Lean readiness first; inspect Numina/backend readiness only when the user asks for an optional Lean-specialist 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. The helper CLI under `skills/lean-runtime/scripts/` is optional shared tooling and should be used only for environment checks, structured validation, optional Numina readiness/setup, patch review, `sorry` detection, or minimal failure handoff. -Deploy or call the official Numina subagent only when the user asks for it or approves it after an explanation. Keep secrets in environment variables or ignored local files. +Deploy or call the official Numina backend only when the user asks for it or approves it after an explanation. Keep secrets in environment variables or ignored local files. diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 54f6b80..0323321 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -16,8 +16,8 @@ jobs: - name: Run unit tests run: | - PYTHONDONTWRITEBYTECODE=1 python -m unittest discover -s skills/lean-formalization/tests + PYTHONDONTWRITEBYTECODE=1 python -m unittest discover -s skills/lean-runtime/tests - name: Verify package shape run: | - PYTHONDONTWRITEBYTECODE=1 python skills/lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests + PYTHONDONTWRITEBYTECODE=1 python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests diff --git a/.opencode/agents/lean-formalization.md b/.opencode/agents/lean-formalization.md index e290655..9f7a5cb 100644 --- a/.opencode/agents/lean-formalization.md +++ b/.opencode/agents/lean-formalization.md @@ -8,6 +8,12 @@ Canonical workflow: skills/lean-formalization/SKILL.md ``` +Shared runtime support: + +```text +skills/lean-runtime/ +``` + Rules: - This is a coding-agent-first Lean skill. diff --git a/AGENTS.md b/AGENTS.md index 5862bb5..d81946e 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -1,21 +1,22 @@ # Agent Instructions Use `skills/lean-setup/SKILL.md` for setup-only tasks such as installing or verifying Lean 4, `elan`, `lake`, or a reusable mathlib workspace. -Use the canonical shared Skill layer at `skills/lean-formalization/SKILL.md` for Lean 4 formalization, proof repair, theorem transcription, `sorry` completion, Lean patch review, official Numina Lean Agent runtime deployment/calls, local Lean validation, and minimal failure handoff. +Use the canonical shared Skill layer at `skills/lean-formalization/SKILL.md` for Lean 4 formalization, proof repair, theorem transcription, `sorry` completion, Lean patch review, optional Lean-specialist backend adapter work currently implemented for official Numina Lean Agent runtime deployment/calls, local Lean validation, and minimal failure handoff. +Reusable scripts, examples, prompts, schemas, and references live in the non-user-facing support layer at `skills/lean-runtime/`; install it alongside the two public Skill entrypoints. Core rules: - This is a coding-agent-first Lean skill. - The coding agent is the primary Lean worker. - Setup-only mode should not ask for a theorem target. -- Official Numina is an optional deployable subagent backend. +- Official Numina is the only currently supported deployable backend adapter; Archon and other backends are future adapters until an adapter contract, setup path, call path, and local validation gates are implemented. - Match the user's language by default. - If the user's language is ambiguous, default to Chinese. - Lead the interaction: inspect context, summarize what is ready, recommend the next useful step, and ask at most one blocking question. - Do not treat a language switch as a task reset; keep the current diagnosis and continue leading in the new language. - When no target is provided, run or propose a safe local smoke/readiness check before asking for more input. - Use the bundled smoke test when no user target is available. -- Formalization/proof readiness should inspect local Lean readiness and Numina subagent readiness separately. +- 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. @@ -27,5 +28,5 @@ Core rules: Useful validation: ```bash -PYTHONDONTWRITEBYTECODE=1 python skills/lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests +PYTHONDONTWRITEBYTECODE=1 python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests ``` diff --git a/CLAUDE.md b/CLAUDE.md index 570ee16..b075794 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -12,7 +12,13 @@ For Lean formalization or proof work in this repository, read and follow the sha skills/lean-formalization/SKILL.md ``` -Use Claude Code as the primary Lean coding agent. Official Numina is an optional deployable subagent backend; preserve that setup/call path but do not make it the default. +Shared helper scripts, references, prompts, schemas, examples, and tests live in: + +```text +skills/lean-runtime/ +``` + +Use Claude Code as the primary Lean coding agent. Official Numina is the only currently supported deployable backend adapter; preserve that setup/call path but do not make it the default. Archon and other backends are future adapters until their setup, call, credential, mutation, and validation contracts are documented. Setup-only mode should create or verify the Lean/mathlib workspace without asking for a theorem target. Match the user's language by default. If the user's language is ambiguous, default to Chinese. @@ -20,9 +26,9 @@ Lead the interaction: inspect context, summarize what is ready, recommend the ne Do not treat a language switch as a task reset; keep the current diagnosis and continue leading in the new language. When no target is provided, run or propose a safe local smoke/readiness check before asking for more input. Use the bundled smoke test when no user target is available. -Formalization/proof readiness should inspect local Lean readiness and Numina subagent readiness separately. +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. -Deploy or call the official Numina subagent runtime only after explanation and approval. Keep secrets in environment variables or ignored local files. +Deploy or call the official Numina backend runtime only after explanation and approval. Keep secrets in environment variables or ignored local files. diff --git a/GEMINI.md b/GEMINI.md index 427b59d..9f25e71 100644 --- a/GEMINI.md +++ b/GEMINI.md @@ -12,7 +12,7 @@ For Lean 4 formal verification tasks, use the shared Skill layer at: skills/lean-formalization/SKILL.md ``` -Use Gemini as the primary Lean coding agent. Official Numina is an optional deployable subagent backend; preserve that setup/call path but do not make it the default. +Use Gemini as the primary Lean coding agent. Official Numina is the only currently supported deployable backend adapter; preserve that setup/call path but do not make it the default. Archon and other backends are future adapters until their setup, call, credential, mutation, and validation contracts are documented. Setup-only mode should create or verify the Lean/mathlib workspace without asking for a theorem target. Match the user's language by default. If the user's language is ambiguous, default to Chinese. @@ -20,9 +20,9 @@ Lead the interaction: inspect context, summarize what is ready, recommend the ne Do not treat a language switch as a task reset; keep the current diagnosis and continue leading in the new language. When no target is provided, run or propose a safe local smoke/readiness check before asking for more input. Use the bundled smoke test when no user target is available. -Formalization/proof readiness should inspect local Lean readiness and Numina subagent readiness separately. +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. -The helper CLI under `skills/lean-formalization/scripts/` is optional tooling. It can report and configure the official Numina subagent runtime, but the agent should still validate final Lean patches locally. +The helper CLI under `skills/lean-runtime/scripts/` is optional tooling shared by the two public Skill entrypoints. It can report and configure the official Numina backend runtime, but the agent should still validate final Lean patches locally. diff --git a/README.md b/README.md index 7b98a5f..ca691e0 100644 --- a/README.md +++ b/README.md @@ -2,8 +2,8 @@ # AI4Math · Lean Agents -Lean 4 setup, formalization, proof repair, patch review, and optional Numina -subagent workflows for coding agents. +Lean 4 setup, formalization, proof repair, patch review, and optional +Lean-specialist backend workflows for coding agents. [中文说明](README.zh-CN.md) · [Contributors](CONTRIBUTORS.md) · [Skill packages](#skill-packages) · [Quick start](#quick-start) · [Security model](#security-and-scope) @@ -20,10 +20,21 @@ setup-only entrypoint and one formalization entrypoint so a coding agent can inspect Lean projects, prepare reusable mathlib workspaces, repair proofs, and validate final patches with evidence. +Both public entrypoints share the bundled `skills/lean-runtime/` support layer +for helper scripts, references, prompts, schemas, examples, and tests. Users +invoke only `lean-setup` or `lean-formalization`; installers should keep +`lean-runtime` next to them. + `lean-formalization` incorporates public Lean-specialist agent patterns such as theorem-state loops, premise retrieval, bounded proof search, validation gates, failure memory, and optional official Numina handoff. These patterns are treated -as workflow mechanisms, not mandatory external services. +as workflow mechanisms, not mandatory external services. The optional Lean-specialist backend +path is explicit: official Numina is the currently supported optional deployable +backend; other backends remain future adapters until setup, call, validation, +and failure-triage contracts are documented. + +Currently supported optional backend: official Numina Lean Agent runtime. +Future backend adapters do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented. ## Skill Packages @@ -32,6 +43,8 @@ as workflow mechanisms, not mandatory external services. | [`lean-setup`](skills/lean-setup/) | Install or verify Lean 4, `elan`, `lake`, and reusable mathlib workspace readiness before proof work. | [`README`](skills/lean-setup/README.md) · [`SKILL`](skills/lean-setup/SKILL.md) | | [`lean-formalization`](skills/lean-formalization/) | Formalize theorem statements, repair Lean proofs, complete `sorry`, review patches, and optionally coordinate Numina runs. | [`README`](skills/lean-formalization/README.md) · [`SKILL`](skills/lean-formalization/SKILL.md) | +`skills/lean-runtime/` is a shared implementation layer, not a user-facing skill. + ## Quick Start Clone the repository and choose the entrypoint: @@ -62,11 +75,13 @@ AI4Math-Lean-Agents/ ├── SKILL.md └── skills/ ├── lean-setup/ - └── lean-formalization/ + ├── lean-formalization/ + └── lean-runtime/ ``` The root `SKILL.md` is a compatibility router. Package-local instructions are -the source of truth for concrete Lean work. +the source of truth for concrete Lean work; shared scripts and references live +under `skills/lean-runtime/`. ## Validation @@ -74,7 +89,7 @@ Use package-local validation when changing Lean logic. The formalization package provides the helper: ```bash -python skills/lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests +python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests ``` At minimum, run the local skill validator on each changed standard skill diff --git a/README.zh-CN.md b/README.zh-CN.md index 764647a..e648d1d 100644 --- a/README.zh-CN.md +++ b/README.zh-CN.md @@ -2,7 +2,7 @@ # AI4Math · Lean Agents -面向 Lean 4 环境准备、形式化、proof repair、patch review 和可选 Numina subagent 的 AI4Math 技能集合。 +面向 Lean 4 环境准备、形式化、proof repair、patch review 和可选 Lean-specialist backend 的 AI4Math 技能集合。 [English](README.md) · [贡献者](CONTRIBUTORS.md) · [技能包](#技能包) · [快速开始](#快速开始) · [安全边界](#安全边界) @@ -16,8 +16,12 @@ 这个仓库是 AI4Math Lean agent 技能入口。它提供一个 setup-only 入口和一个 formalization 入口，让 coding agent 可以检查 Lean 项目、准备可复用 mathlib workspace、修复证明，并用证据验证最终 patch。 +两个公开入口共享仓库内的 `skills/lean-runtime/` 支持层。这里放 helper scripts、references、prompts、schemas、examples 和 tests。用户只调用 `lean-setup` 或 `lean-formalization`；安装时应把 `lean-runtime` 作为相邻支持目录保留。 + `lean-formalization` 借鉴公开 Lean-specialist agent 机制，例如 theorem-state loop、premise retrieval、bounded proof search、validation gate、failure memory 和可选官方 Numina handoff。这些是工作流机制，不是强制外部服务。 +可选 Lean 专用 agent backend 当前只记录已经验证过的运行路径。当前支持的可选 backend：official Numina Lean Agent runtime。未来 backend adapter 需要等 setup、调用、验证和 failure triage 合约文档化后再宣称支持；不要写成已支持。 + ## 技能包 | 包 | 适用任务 | 入口 | @@ -25,6 +29,8 @@ | [`lean-setup`](skills/lean-setup/) | 安装或验证 Lean 4、`elan`、`lake` 和可复用 mathlib workspace，就绪后再进入证明工作。 | [`README`](skills/lean-setup/README.md) · [`SKILL`](skills/lean-setup/SKILL.md) | | [`lean-formalization`](skills/lean-formalization/) | 形式化 theorem statement、修复 Lean proof、完成 `sorry`、审查 patch，并在需要时协调 Numina。 | [`README`](skills/lean-formalization/README.md) · [`SKILL`](skills/lean-formalization/SKILL.md) | +`skills/lean-runtime/` 是共享实现层，不是用户直接调用的 skill。 + ## 快速开始 克隆仓库并选择入口： @@ -55,17 +61,18 @@ AI4Math-Lean-Agents/ ├── SKILL.md └── skills/ ├── lean-setup/ - └── lean-formalization/ + ├── lean-formalization/ + └── lean-runtime/ ``` -根 `SKILL.md` 是兼容路由层。具体 Lean 工作以包内说明为准。 +根 `SKILL.md` 是兼容路由层。具体 Lean 工作以包内说明为准；共享脚本和 references 位于 `skills/lean-runtime/`。 ## 验证 修改 Lean 逻辑时优先使用包内验证。formalization 包提供： ```bash -python skills/lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests +python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests ``` 至少应对变更过的标准技能包运行本地 skill validator，并检查 README 链接。 diff --git a/SKILL.md b/SKILL.md index 3890219..8d7ca98 100644 --- a/SKILL.md +++ b/SKILL.md @@ -1,6 +1,6 @@ --- name: lean-formalization -description: Use when a coding agent needs Lean 4 formalization, proof repair, theorem transcription, sorry completion, Lean patch review, optional official Numina deployment/calls, or local Lean validation. +description: Use when a coding agent needs Lean 4 formalization, proof repair, theorem transcription, sorry completion, Lean patch review, optional Lean-specialist backend adapter work currently implemented for official Numina deployment/calls, or local Lean validation. --- # Lean Formalization @@ -15,6 +15,12 @@ skills/lean-formalization/SKILL.md Read that concrete Skill before formalization or proof work. Keep platform adapters thin and improve the shared Skill layer first. +Reusable scripts, prompts, examples, references, schemas, and tests live in: + +```text +skills/lean-runtime/ +``` + For setup-only tasks such as installing Lean, checking `elan`/`lake`, or creating a reusable mathlib workspace, use: @@ -26,5 +32,5 @@ skills/lean-setup/SKILL.md - Preserve theorem statements unless the user approves a change. - Reject final patches containing `sorry`, `admit`, or newly introduced `axiom`. -- Explain and approve optional Numina runtime setup before executing it. +- Explain and approve optional backend runtime setup before executing it; currently supported optional backend: official Numina Lean Agent runtime. - Validate final Lean patches locally when possible. diff --git a/skills/lean-formalization/README.md b/skills/lean-formalization/README.md index 6784d26..d4bd6f7 100644 --- a/skills/lean-formalization/README.md +++ b/skills/lean-formalization/README.md @@ -1,32 +1,29 @@ # Lean Formalization -`lean-formalization` is the concrete AI4Math skill package for Lean 4 +`lean-formalization` is the concrete AI4Math skill entrypoint for Lean 4 formalization, proof repair, theorem transcription, `sorry` completion, Lean -patch review, local validation, and optional official Numina runtime work. +patch review, local validation, and optional Lean-specialist backend adapter +work currently implemented for official Numina. ## Entry Point Start with [`SKILL.md`](SKILL.md). It defines the coding-agent-first workflow, -the optional Numina boundary, safety rules, and the reference files to load for -specific tasks. +the optional backend boundary, safety rules, and the reference files to load +for specific tasks. -## Package Layout +## Runtime Support -- `scripts/`: helper CLI commands for environment checks, validation, patch - review, Numina setup, and delivery verification. -- `references/`: task-specific guidance for direct Lean workflows, runtime - configuration, Numina, review, and failure reporting. -- `prompts/`: reusable task envelopes for formalization, proof repair, and - `sorry` completion. -- `config/` and `schemas/`: example configuration and validation schemas. -- `tests/`: package-level Python tests for the helper CLI and validation logic. +The reusable implementation lives in the sibling `../lean-runtime/` support +layer. It contains helper scripts, task-specific references, prompts, examples, +schemas, configuration templates, and tests. Keep `lean-runtime` installed next +to this entrypoint. ## Validation Run from the repository root: ```bash -PYTHONDONTWRITEBYTECODE=1 python skills/lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests +PYTHONDONTWRITEBYTECODE=1 python skills/lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests ``` ## Related Work and Public References diff --git a/skills/lean-formalization/SKILL.md b/skills/lean-formalization/SKILL.md index 02ab218..505baf5 100644 --- a/skills/lean-formalization/SKILL.md +++ b/skills/lean-formalization/SKILL.md @@ -1,43 +1,45 @@ --- name: lean-formalization -description: Use for interactive Lean 4 formal verification by coding agents with reusable Lean/mathlib workspaces, theorem formalization, proof repair, sorry completion, patch review, optional official Numina subagent deployment/calls, and minimal failure handoff. +description: Use for interactive Lean 4 formal verification by coding agents with reusable Lean/mathlib workspaces, theorem formalization, proof repair, sorry completion, patch review, optional Lean-specialist backend adapter support currently implemented for official Numina deployment/calls, and minimal failure handoff. --- # Lean Formalization -Use this skill when the user wants a coding agent to do Lean 4 formalization, proof repair, theorem transcription, sorry completion, review of a Lean patch, or optional official Numina Lean Agent/subagent work. +Use this skill when the user wants a coding agent to do Lean 4 formalization, proof repair, theorem transcription, sorry completion, review of a Lean patch, or optional Lean-specialist backend work. If the user only wants Lean 4, `elan`, `lake`, or a reusable mathlib workspace configured, use the sibling `../lean-setup/SKILL.md` entrypoint and do not ask for a theorem target. +Shared scripts, prompts, schemas, examples, and references live in the non-user-facing `../lean-runtime/` support layer. Treat `lean-setup` and `lean-formalization` as the two public entrypoints; do not ask users to invoke `lean-runtime` directly. + This is a coding-agent-first Lean skill. The coding agent is the primary Lean worker. It reads and edits Lean files, runs Lean/Lake checks, diagnoses errors, preserves theorem statements, and iterates with the user. Default execution mode is coding-agent mode. Incorporate publicly documented Lean-specialist agent patterns into the default coding-agent workflow. Use systems such as Numina, LeanDojo/ReProver, LeanCopilot, COPRA-style proof search, Lean LSP, MCP, and lightweight iterative proof agents as related-work references for mechanisms such as project gating, statement normalization, theorem-state loops, premise retrieval, bounded tactic/proof search, validation oracles, failure memory, and minimized handoff. Treat specialist-agent patterns as mechanisms, not mandatory external services. -Official Numina is an optional deployable subagent backend. Keep the official Numina deployment/call path available for users who ask for the official Lean Agent, batch proof search, or an external subagent run. Use Numina when the user asks for the official Lean Agent, batch proof search, or an external subagent run. +Lean-specialist backend adapters are optional escalation paths. Currently supported optional backend: official Numina Lean Agent runtime. Official Numina is the only currently supported deployable backend adapter; Archon and other backends are future adapters until an adapter contract, setup path, call path, and local validation gates are implemented. Future backend adapters may include Archon or other Lean-specialist systems, but do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented. Use the official Numina adapter only when the user asks for the official Lean Agent, Numina, batch proof search, or an approved external subagent run. Match the user's language by default. If the user's language is ambiguous, default to Chinese. If the user writes Chinese, respond in Chinese from the first turn unless they ask otherwise. A language switch is not a task reset. Keep the current environment state, prior diagnosis, and recommended next action, then continue leading in the new language. Lead the interaction; do not wait for the user to drive every step. When the user's request is broad or underspecified, first orient yourself to the Lean project/workspace state, then propose the next useful action in plain language. Do not open with a passive "send me the file" checklist when you can inspect context or offer a concrete starting path. -If no target is available, run or propose a safe local smoke/readiness check. Use the bundled smoke test when no user target is available. Then recommend a default path, such as checking the shared Lean workspace, running the built-in smoke theorem, inspecting a Lean project, or checking Numina subagent readiness if the user wants that path. Avoid ending with only "send me a file" or an equivalent passive handoff. +If no target is available, run or propose a safe local smoke/readiness check. Use the bundled smoke test when no user target is available. Then recommend a default path, such as checking the shared Lean workspace, running the built-in smoke theorem, or inspecting a Lean project. Check backend readiness only when the user wants an optional Lean-specialist backend path. Avoid ending with only "send me a file" or an equivalent passive handoff. The bundled CLI is a helper toolbox, not the workflow driver. Prefer normal coding-agent judgment, direct file edits, `rg`, Lean/Lake validation, and repository context. Use helper commands only when their deterministic output is useful. -Use official Numina through a human-in-the-loop subagent workflow. Numina lives under shared local state at `${AI4MATH_HOME:-~/.ai4math}/numina-runtime/`; the coding agent explains clone, setup, API-key, proxy/MCP, and upstream runner implications before running setup or calling the official runner. Do not turn helper commands into a closed proof workflow. +Use official Numina through a human-in-the-loop backend adapter workflow. Numina lives under shared local state at `${AI4MATH_HOME:-~/.ai4math}/numina-runtime/`; the coding agent explains clone, setup, API-key, proxy/MCP, and upstream runner implications before running setup or calling the official runner. Future backend adapters must follow `../lean-runtime/references/backend_adapter_checklist.md`. Do not turn helper commands into a closed proof workflow. -Opening readiness should inspect local Lean readiness and Numina subagent readiness separately. 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. +Opening readiness should inspect local Lean readiness first; inspect Numina or another backend readiness only when the user asks for an optional Lean-specialist backend. Do not require API keys for the default coding-agent path. Default coding-agent Lean work must not require any backend adapter. Shared workspace is the default Lean project context; Numina may target it instead of upstream examples. -Do not remove the official Numina subagent path. Treat it as an optional backend with explicit approval, while keeping the direct coding-agent Lean workflow useful without external APIs. +Do not remove the official Numina subagent path. Treat it as the supported optional backend with explicit approval, while keeping the direct coding-agent Lean workflow useful without external APIs. ## Agent Playbook 1. Start by orienting the session: inspect the current repository/workspace when possible, distinguish existing Lake project, shared Lean workspace, local Lean validation readiness, Numina runtime, and Numina credentials/auth, and summarize what is already usable. Treat upstream Numina example projects as demos only; do not let their pinned `lean-toolchain` make the shared workspace look broken. -2. If the user has not provided a precise target, offer a small next-step menu such as run the bundled smoke test, repair an existing Lean file, formalize a natural-language/LaTeX theorem, inspect a Lean project, configure Numina credentials, run a Numina readiness check, or prepare the shared workspace as a Numina target. Recommend one default path based on what inspection found. +2. If the user has not provided a precise target, offer a small next-step menu such as run the bundled smoke test, repair an existing Lean file, formalize a natural-language/LaTeX theorem, or inspect a Lean project. Include Numina readiness or credential setup only when the user asks for the optional official backend path. Recommend one default path based on what inspection found. 3. Ask at most one blocking question at a time. Prefer a concrete recommendation plus one decision question over a list of required inputs. -4. Understand the user's intent: direct coding-agent repair/formalization, configure Numina, call Numina, repair a file, formalize a statement, prove a target, complete `sorry`, review a patch, batch a folder, or minimize a failure. +4. Understand the user's intent: direct coding-agent repair/formalization, configure the supported official Numina backend, call Numina, repair a file, formalize a statement, prove a target, complete `sorry`, review a patch, batch a folder, or minimize a failure. 5. Locate the relevant Lean project, files, declarations, imports, and current errors. Use the user's existing Lake project when available; otherwise use the shared workspace as the coding-agent project context and optional Numina target project. 6. For standalone files, use or create the shared workspace `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`; do not create a second project-local workspace unless the user asks for isolation. -7. When reporting readiness, lead with local Lean readiness, then Numina subagent readiness. If Numina credentials are missing, say that only the optional Numina subagent path needs configuration. +7. When reporting readiness, lead with local Lean readiness. Report Numina readiness only when the optional official backend path is requested. If Numina credentials are missing, say that only the optional Numina backend path needs configuration. 8. Before a Numina setup or run, inspect `doctor` readiness, explain the deployment/call, target project, prompt, result directory, credential/proxy/MCP state, and local validation plan; proceed only after approval. 9. For natural-language or LaTeX input, draft the Lean declaration and ask for confirmation before long proof work. 10. Edit Lean directly in small steps for the default coding-agent path, using incorporated specialist-agent patterns such as theorem-state inspection, nearby lemma retrieval, bounded proof attempts, failed-strategy notes, and minimal failure extraction. If Numina is approved, call the official Numina runner for proof search/formalization, then run Lean/Lake validation and patch safety checks before accepting results. @@ -47,23 +49,23 @@ Do not remove the official Numina subagent path. Treat it as an optional backend ## Helper Toolbox -Use `python scripts/ai4m_lean.py ` when it saves effort or reduces risk: +Use `python ../lean-runtime/scripts/ai4m_lean.py ` when it saves effort or reduces risk: -- `env` / `doctor`: inspect Lean workspace, local tool availability, and Numina subagent readiness. +- `env` / `doctor`: inspect Lean workspace, local tool availability, and supported Numina backend readiness. - `configure --create-workspace`: create or reuse the shared managed workspace. - `configure --setup-numina --project-name `: after user approval, clone/configure the official Numina runtime under `${AI4MATH_HOME:-~/.ai4math}/numina-runtime/`. -- `smoke-test`: run the bundled `examples/smoke/NuminaSmoke.lean` target in the shared workspace without external API calls. +- `smoke-test`: run the bundled `../lean-runtime/examples/smoke/NuminaSmoke.lean` target in the shared workspace without external API calls. - `check`: run a structured Lean/Lake validation. - `review` / `detect-sorry`: guard against placeholders, axioms, and statement drift. - `minimize-failure`: extract a compact failing Lean fragment. -- `prove` / `formalize` / `repair` / `complete-sorries` / `batch`: optional dry-run task envelopes for coding-agent bookkeeping; use the official Numina runner only when the optional subagent path is approved. +- `prove` / `formalize` / `repair` / `complete-sorries` / `batch`: optional dry-run task envelopes for coding-agent bookkeeping; use the official Numina runner only when the optional backend path is approved. - `verify-delivery`: validate this skill package. All helper commands emit machine-readable JSON on stdout. Human-readable diagnostics go to stderr or log files. ## Numina Runtime -When using the official Numina runtime, follow `references/numina_runtime.md`. For auth/proxy/MCP/failure triage, follow `references/numina_subagent_troubleshooting.md`. Proof strategy is a human-in-the-loop process with the user, the coding agent, local Lean checks, and, when approved, the official Numina runner as an optional subagent backend. +When using the official Numina runtime, follow `../lean-runtime/references/numina_runtime.md`. For auth/proxy/MCP/failure triage, follow `../lean-runtime/references/numina_subagent_troubleshooting.md`. For future backend adapters, follow `../lean-runtime/references/backend_adapter_checklist.md`. Proof strategy is a human-in-the-loop process with the user, the coding agent, local Lean checks, and, when approved, the official Numina runner as the currently supported optional backend. ## Safety Rules @@ -79,12 +81,13 @@ When using the official Numina runtime, follow `references/numina_runtime.md`. F ## References -- Read `references/direct_lean_workflow.md` for the default coding-agent proof/repair/formalization loop. -- Read `references/specialist_agent_patterns.md` when adapting ideas from Numina, LeanDojo/ReProver, LeanCopilot, COPRA-style proof search, Lean LSP/MCP, or other Lean-specialist agents. -- Read `references/lean_runtime_configuration.md` when setting up or diagnosing the reusable Lean workspace. -- Read `references/numina_runtime.md` when the user wants the official Numina deployment/call path. -- Read `references/numina_subagent_troubleshooting.md` when Numina auth, proxy, MCP, or runner failures appear. -- Read `references/interactive_orchestration.md` when guiding user intake and task decomposition. -- Read `references/review_checklist.md` before accepting a Lean patch. -- Read `references/failure_taxonomy.md` when reporting a blocked proof. -- Read `references/numina_reverse_analysis.md` when explaining which Numina mechanisms are incorporated locally and which are delegated to the optional official runtime. +- Read `../lean-runtime/references/direct_lean_workflow.md` for the default coding-agent proof/repair/formalization loop. +- Read `../lean-runtime/references/specialist_agent_patterns.md` when adapting ideas from Numina, LeanDojo/ReProver, LeanCopilot, COPRA-style proof search, Lean LSP/MCP, or other Lean-specialist agents. +- Read `../lean-runtime/references/lean_runtime_configuration.md` when setting up or diagnosing the reusable Lean workspace. +- Read `../lean-runtime/references/numina_runtime.md` when the user wants the official Numina deployment/call path. +- Read `../lean-runtime/references/numina_subagent_troubleshooting.md` when Numina auth, proxy, MCP, or runner failures appear. +- Read `../lean-runtime/references/backend_adapter_checklist.md` before describing Archon or any other future backend as supported. +- Read `../lean-runtime/references/interactive_orchestration.md` when guiding user intake and task decomposition. +- Read `../lean-runtime/references/review_checklist.md` before accepting a Lean patch. +- Read `../lean-runtime/references/failure_taxonomy.md` when reporting a blocked proof. +- Read `../lean-runtime/references/numina_reverse_analysis.md` when explaining which Numina mechanisms are incorporated locally and which are delegated to the optional official runtime. diff --git a/skills/lean-formalization/agents/openai.yaml b/skills/lean-formalization/agents/openai.yaml index 88540b8..a45bf9b 100644 --- a/skills/lean-formalization/agents/openai.yaml +++ b/skills/lean-formalization/agents/openai.yaml @@ -1,3 +1,3 @@ display_name: Lean Formalization -short_description: Interactive Lean 4 verification for coding agents that incorporate Lean-specialist agent patterns, with optional official Numina subagent calls. -default_prompt: 请用中文开始并主动引导 Lean 会话；如果用户明确使用其他语言，再切换到用户语言。默认走 coding agent Lean 工作流：你直接读写 Lean、运行 Lean/Lake、根据报错迭代并验收无 sorry/admit/axiom。该 skill 参考并整合 Numina、LeanDojo/ReProver、LeanCopilot、COPRA-style proof search、Lean LSP/MCP 等公开 Lean 专用 agent 的机制：项目门禁、statement normalization、theorem-state loop、premise retrieval、bounded search、失败记忆、Lean/Lake oracle 和 minimal failure handoff。Numina 是可部署的可选 subagent backend；只有用户要求 official Lean Agent、Numina、batch proof search 或外部 subagent 时才进入这条链路。开场分别检查本地 Lean/shared workspace readiness 和 Numina subagent readiness。没有用户目标时先使用内置 smoke-test 验证本地 Lean/mathlib 验收链路。默认 coding-agent 路径不要求 API key；Numina subagent 调用前要说明 target、prompt、max rounds、result dir、Claude/API/proxy/MCP 状态并获得批准。一次最多问一个阻塞问题。 +short_description: Interactive Lean 4 verification for coding agents that incorporate Lean-specialist agent patterns, with optional backend adapter support currently implemented for official Numina. +default_prompt: 请用中文开始并主动引导 Lean 会话；如果用户明确使用其他语言，再切换到用户语言。默认走 coding agent Lean 工作流：你直接读写 Lean、运行 Lean/Lake、根据报错迭代并验收无 sorry/admit/axiom。该 skill 参考并整合 Numina、LeanDojo/ReProver、LeanCopilot、COPRA-style proof search、Lean LSP/MCP 等公开 Lean 专用 agent 的机制：项目门禁、statement normalization、theorem-state loop、premise retrieval、bounded search、失败记忆、Lean/Lake oracle 和 minimal failure handoff。可选 Lean 专用 backend adapter 目前只承诺 official Numina adapter 已支持；Archon 和其他 backend 只能作为 future adapters，除非部署、readiness、调用、validation、failure triage 已文档化。只有用户要求 official Lean Agent、Numina、batch proof search 或外部 subagent 时才进入 backend 链路。默认开场检查本地 Lean/shared workspace readiness；仅当用户要求 optional backend 时再检查 Numina readiness。没有用户目标时先使用内置 smoke-test 验证本地 Lean/mathlib 验收链路。默认 coding-agent 路径不要求 API key；Numina backend 调用前要说明 target、prompt、max rounds、result dir、Claude/API/proxy/MCP 状态并获得批准。一次最多问一个阻塞问题。 diff --git a/skills/lean-formalization/config/env.example b/skills/lean-runtime/config/env.example similarity index 100% rename from skills/lean-formalization/config/env.example rename to skills/lean-runtime/config/env.example diff --git a/skills/lean-formalization/config/lean_agent.example.toml b/skills/lean-runtime/config/lean_agent.example.toml similarity index 100% rename from skills/lean-formalization/config/lean_agent.example.toml rename to skills/lean-runtime/config/lean_agent.example.toml diff --git a/skills/lean-formalization/config/numina_runtime.example.toml b/skills/lean-runtime/config/numina_runtime.example.toml similarity index 100% rename from skills/lean-formalization/config/numina_runtime.example.toml rename to skills/lean-runtime/config/numina_runtime.example.toml diff --git a/skills/lean-formalization/examples/smoke/NuminaSmoke.lean b/skills/lean-runtime/examples/smoke/NuminaSmoke.lean similarity index 100% rename from skills/lean-formalization/examples/smoke/NuminaSmoke.lean rename to skills/lean-runtime/examples/smoke/NuminaSmoke.lean diff --git a/skills/lean-formalization/prompts/complete_sorries.md b/skills/lean-runtime/prompts/complete_sorries.md similarity index 100% rename from skills/lean-formalization/prompts/complete_sorries.md rename to skills/lean-runtime/prompts/complete_sorries.md diff --git a/skills/lean-formalization/prompts/formalize_statement.md b/skills/lean-runtime/prompts/formalize_statement.md similarity index 100% rename from skills/lean-formalization/prompts/formalize_statement.md rename to skills/lean-runtime/prompts/formalize_statement.md diff --git a/skills/lean-formalization/prompts/prove_theorem.md b/skills/lean-runtime/prompts/prove_theorem.md similarity index 100% rename from skills/lean-formalization/prompts/prove_theorem.md rename to skills/lean-runtime/prompts/prove_theorem.md diff --git a/skills/lean-formalization/prompts/repair_lean_file.md b/skills/lean-runtime/prompts/repair_lean_file.md similarity index 100% rename from skills/lean-formalization/prompts/repair_lean_file.md rename to skills/lean-runtime/prompts/repair_lean_file.md diff --git a/skills/lean-runtime/references/backend_adapter_checklist.md b/skills/lean-runtime/references/backend_adapter_checklist.md new file mode 100644 index 0000000..7c2151d --- /dev/null +++ b/skills/lean-runtime/references/backend_adapter_checklist.md @@ -0,0 +1,31 @@ +# Backend Adapter Checklist + +Use this checklist before claiming that a Lean-specialist backend is supported. Backend adapters are optional escalation paths; default coding-agent Lean work must not require any backend adapter. + +## Support Status + +- `supported`: setup, readiness checks, invocation, local validation, and failure triage are documented and guarded. +- `experimental`: partial adapter exists, but the agent must explain gaps and request approval before use. +- `future`: related work or candidate backend only; do not claim support or call it automatically. + +Currently supported optional backend: official Numina Lean Agent runtime. + +Future backend adapters may include Archon or other Lean-specialist systems, but do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented. + +## Adapter Contract + +Document all of the following before moving a backend out of `future`: + +- Name, upstream source, license, and support status. +- Trigger phrases that justify using this backend. +- Setup location, install commands, network access, and local state written. +- Required tools, credentials, API keys, proxy settings, or MCP scope. +- Readiness checks that do not call external model APIs. +- Invocation command, working directory, target project/file/folder, prompt, result directory, and round limits. +- Mutation boundary: which files may be changed, where generated outputs go, and which actions require approval. +- Local validation gate: Lean/Lake check, `detect-sorry`, `review`, and theorem statement drift checks. +- Failure triage: auth, proxy, MCP, toolchain, runner, timeout, and fallback to the coding-agent path. + +## Non-Claim Rule + +Do not claim support for a backend adapter unless its setup, call, credential, mutation, and validation contracts are documented. Unimplemented adapters may be cited as related work or future adapters only. diff --git a/skills/lean-formalization/references/direct_lean_workflow.md b/skills/lean-runtime/references/direct_lean_workflow.md similarity index 92% rename from skills/lean-formalization/references/direct_lean_workflow.md rename to skills/lean-runtime/references/direct_lean_workflow.md index aeb3d22..a5fb44d 100644 --- a/skills/lean-formalization/references/direct_lean_workflow.md +++ b/skills/lean-runtime/references/direct_lean_workflow.md @@ -1,6 +1,6 @@ # Direct Coding-Agent Lean Workflow -This is the default workflow. The coding agent reads and edits Lean directly, runs Lean/Lake checks, and iterates from concrete errors/goals. It incorporates Lean-specialist agent patterns into local work: theorem-state loops, premise retrieval, bounded proof attempts, failed-strategy memory, and minimal failure handoff. Official Numina remains available as an optional deployable subagent backend, but it is not required for ordinary Lean formalization, proof repair, or sorry completion. +This is the default workflow. The coding agent reads and edits Lean directly, runs Lean/Lake checks, and iterates from concrete errors/goals. It incorporates Lean-specialist agent patterns into local work: theorem-state loops, premise retrieval, bounded proof attempts, failed-strategy memory, and minimal failure handoff. Official Numina remains available as the currently supported optional Lean-specialist backend adapter, but it is not required for ordinary Lean formalization, proof repair, or sorry completion. ## Guidance-First Loop @@ -27,7 +27,7 @@ Use helpers for mechanical checks: - failure handoff: `minimize-failure`; - package QA: `verify-delivery`. -Do not route creative proof search through helper commands. `prove`, `formalize`, `repair`, `complete-sorries`, and `batch` only produce optional task envelopes for bookkeeping. Use the official Numina runner only when the optional subagent path is approved. +Do not route creative proof search through helper commands. `prove`, `formalize`, `repair`, `complete-sorries`, and `batch` only produce optional task envelopes for bookkeeping. Use the official Numina runner only when the optional backend path is approved. ## Workspace Choice diff --git a/skills/lean-formalization/references/failure_taxonomy.md b/skills/lean-runtime/references/failure_taxonomy.md similarity index 100% rename from skills/lean-formalization/references/failure_taxonomy.md rename to skills/lean-runtime/references/failure_taxonomy.md diff --git a/skills/lean-formalization/references/interactive_orchestration.md b/skills/lean-runtime/references/interactive_orchestration.md similarity index 69% rename from skills/lean-formalization/references/interactive_orchestration.md rename to skills/lean-runtime/references/interactive_orchestration.md index bd85e4d..c0f6fe6 100644 --- a/skills/lean-formalization/references/interactive_orchestration.md +++ b/skills/lean-runtime/references/interactive_orchestration.md @@ -1,14 +1,14 @@ # Interactive Orchestration -The coordinating coding agent owns user interaction, Lean proof/formalization work, incorporated Lean-specialist agent patterns, optional Numina orchestration, and final validation. It can delegate proof search/formalization to the official Numina subagent when the user asks for that backend. +The coordinating coding agent owns user interaction, Lean proof/formalization work, incorporated Lean-specialist agent patterns, optional Lean-specialist backend adapter orchestration, and final validation. It can delegate proof search/formalization to the official Numina adapter when the user asks for that currently supported backend. -This reference covers the guidance layer: session opening, intake, task classification, direct coding-agent Lean work, specialist-agent pattern selection, optional Numina deployment/calls, local Lean validation, result review, bounded iteration, and minimal failure handoff. +This reference covers the guidance layer: session opening, intake, task classification, direct coding-agent Lean work, specialist-agent pattern selection, optional Lean-specialist backend adapter deployment/calls currently only for official Numina, local Lean validation, result review, bounded iteration, and minimal failure handoff. ## Session Opening If the user's language is ambiguous, default to Chinese. The skill display name, repository name, or command name is not enough evidence to choose English. -This is a coding-agent-first Lean skill. Official Numina is an optional deployable subagent backend. +This is a coding-agent-first Lean skill. Official Numina is the only currently supported deployable backend adapter; Archon and other backends are future adapters until an adapter contract, setup path, call path, and local validation gates are implemented. The default coding-agent path should still absorb Lean-specialist agent mechanisms: project gating, statement normalization, theorem-state loops, premise retrieval, bounded proof search, failed-strategy memory, Lean/Lake validation, and minimized failure handoff. @@ -17,10 +17,10 @@ Lead the interaction; do not wait for the user to drive every step. On a broad r - inspect whether the current directory is a Lake project; - check whether the shared `${AI4MATH_HOME:-~/.ai4math}/lean-workspace` exists; - inspect local Lean/Lake readiness and shared workspace state; -- inspect Numina runtime, upstream checkout, tools, and credential/auth readiness separately; +- inspect Numina runtime, upstream checkout, tools, and credential/auth readiness only when the user asks for the optional official backend; - say what can be done immediately and what would require confirmation. -Opening readiness should inspect local Lean readiness and Numina subagent readiness separately. 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. +Opening readiness should inspect local Lean readiness first. Inspect Numina or another backend readiness only when the user asks for an optional Lean-specialist 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. When checking Numina, distinguish runtime readiness from upstream demo readiness. The runtime can be usable with the shared Lean workspace even if an upstream example or benchmark pins a different `lean-toolchain`. Report that as an example-project issue, not as a failure of the shared environment. @@ -34,10 +34,10 @@ If no precise target is provided, offer a small menu and recommend one path. For - repair or complete an existing Lean file with the coding agent; - formalize a natural-language or LaTeX theorem with the coding agent; - inspect a Lean/Lake project and summarize readiness; -- configure missing Numina credentials/auth; -- run a Numina readiness check; -- prepare the shared workspace as the Numina target project; -- call Numina on a natural-language/LaTeX theorem or Lean file. +- if the user asks for the optional official backend, configure missing Numina credentials/auth; +- if the user asks for the optional official backend, run a Numina readiness check; +- if the user asks for the optional official backend, prepare the shared workspace as the Numina target project; +- if the user asks for the optional official backend, call Numina on a natural-language/LaTeX theorem or Lean file. Ask at most one blocking question at a time. A good opening ends with one decision question, not a checklist. @@ -49,23 +49,25 @@ Ask only when not inferable: - What target file/folder and declaration should be used? - Is changing the theorem statement allowed? - Should standalone work use the reusable managed workspace? -- Should we configure/call Numina now, or only inspect readiness? +- If you want the optional official backend, should we configure/call Numina now, or only inspect readiness? - For natural-language or LaTeX input, what statement should be considered authoritative? Prefer asking these only after orientation. If the repository already reveals the likely next step, state the recommendation and ask for confirmation. ## Decomposition -Break large requests into small Lean targets that the coding agent can work on directly, and that Numina can run against if the optional subagent path is approved. Each target should be checkable afterward with Lean/Lake commands or the helper `check` command. +Break large requests into small Lean targets that the coding agent can work on directly, and that Numina can run against if the optional backend path is approved. Each target should be checkable afterward with Lean/Lake commands or the helper `check` command. For natural-language or LaTeX statements, draft the Lean declaration first and ask for confirmation before long proof work. Once the declaration is confirmed, treat statement preservation as a hard guardrail. -## Numina Run +## Backend Run Before an official Numina call, state the target project/file, prompt file, max rounds, result directory, credential/proxy/MCP state, and validation plan. Ask for approval before any external model call or runtime mutation. After Numina returns, inspect changed Lean files, run local Lean/Lake validation, and reject results containing `sorry`, `admit`, new `axiom`, or unapproved theorem statement changes. +Future backend adapters must satisfy `backend_adapter_checklist.md` before they are described as supported or called. + ## Iteration Policy Stop when: @@ -73,7 +75,7 @@ Stop when: - validation succeeds without `sorry`, `admit`, or new `axiom`; - max local iterations are reached; - Lean workspace setup is missing or broken; -- optional Numina credentials/auth are missing and the user specifically requires Numina; +- official Numina backend credentials/auth are missing and the user specifically requires Numina; - the remaining error requires a human mathematical decision; - the only path forward would weaken the theorem statement without approval. diff --git a/skills/lean-formalization/references/lean_runtime_configuration.md b/skills/lean-runtime/references/lean_runtime_configuration.md similarity index 69% rename from skills/lean-formalization/references/lean_runtime_configuration.md rename to skills/lean-runtime/references/lean_runtime_configuration.md index f4cb8e3..93544d1 100644 --- a/skills/lean-formalization/references/lean_runtime_configuration.md +++ b/skills/lean-runtime/references/lean_runtime_configuration.md @@ -1,6 +1,6 @@ # Lean Runtime Configuration -This skill uses a coding-agent Lean workflow by default. Local Lean/Lake is the primary validation layer. Official Numina is an optional deployable subagent backend under ignored shared local state; see `numina_runtime.md` for deployment and call details. +This skill uses a coding-agent Lean workflow by default. Local Lean/Lake is the primary validation layer. Official Numina is the currently supported optional Lean-specialist backend adapter under ignored shared local state; see `numina_runtime.md` for deployment and call details. ## Shared Layout @@ -13,25 +13,25 @@ ${AI4MATH_HOME:-~/.ai4math}/ └── failures/ ``` -Repository-local machine settings still live under `/.ai4math/` and should not be committed. The reusable Lean workspace and optional Numina runtime are shared by default so standalone tasks do not create a fresh workspace in every project. +Repository-local machine settings still live under `/.ai4math/` and should not be committed. The reusable Lean workspace and supported official Numina backend runtime are shared by default so standalone tasks do not create a fresh workspace in every project. ## Tool Checks Use: ```bash -python scripts/ai4m_lean.py doctor --cwd . -python scripts/ai4m_lean.py env --cwd . +python skills/lean-runtime/scripts/ai4m_lean.py doctor --cwd . +python skills/lean-runtime/scripts/ai4m_lean.py env --cwd . ``` -Required default workflow tools are `git`, `python3`, `elan`, `lean`, and `lake`. Numina setup additionally reports `curl`, `uv`, and `claude` readiness. Official Numina subagent calls need a working Claude CLI/auth path and may need additional API keys for search/tool skills. +Required default workflow tools are `git`, `python3`, `elan`, `lean`, and `lake`. Numina setup additionally reports `curl`, `uv`, and `claude` readiness. Official Numina backend calls need a working Claude CLI/auth path and may need additional API keys for search/tool skills. ## Reusable Lean Workspace For standalone tasks, prefer `${AI4MATH_HOME:-~/.ai4math}/lean-workspace`. Create it once with: ```bash -python 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 --toolchain leanprover/lean4:v4.28.0 ``` Equivalent Lake commands: diff --git a/skills/lean-formalization/references/numina_reverse_analysis.md b/skills/lean-runtime/references/numina_reverse_analysis.md similarity index 89% rename from skills/lean-formalization/references/numina_reverse_analysis.md rename to skills/lean-runtime/references/numina_reverse_analysis.md index f26dcd8..0714b29 100644 --- a/skills/lean-formalization/references/numina_reverse_analysis.md +++ b/skills/lean-runtime/references/numina_reverse_analysis.md @@ -8,11 +8,11 @@ This reference records how this coding-agent Lean skill incorporates mechanisms - Result repository: https://github.com/project-numina/Numina-Putnam2025 - Paper reference: https://arxiv.org/abs/2601.14027 -The goal is not to copy Numina prompts or reimplement Numina proof search. The goal is to incorporate reusable Lean-agent mechanisms into a comprehensive coding-agent skill while preserving a deployable path to the official Numina runtime when the user wants a subagent. +The goal is not to copy Numina prompts or reimplement Numina proof search. The goal is to incorporate reusable Lean-agent mechanisms into a comprehensive coding-agent skill while preserving a deployable path to the official Numina runtime as the currently supported optional backend adapter. ## Incorporated Patterns -1. Use a coding agent as the primary Lean worker, with Numina available as an optional subagent. +1. Use a coding agent as the primary Lean worker, with Numina available as the supported optional backend adapter. 2. Keep Lean/Lake validation as the correctness oracle. 3. Treat theorem statement preservation as a first-class safety check. 4. Work in bounded rounds with a clear stopping condition. @@ -22,7 +22,7 @@ The goal is not to copy Numina prompts or reimplement Numina proof search. The g ## Optional Runtime State -The default AI4Math coding-agent loop does not require these runtime dependencies, but the optional official Numina subagent path does: +The default AI4Math coding-agent loop does not require these runtime dependencies, but the supported official Numina backend path does: - upstream Numina repository checkout; - Numina Python environment; @@ -43,9 +43,9 @@ flowchart TD D --> E["Run Lean/Lake check"] E --> F{"Verified without unsafe placeholders?"} F -->|yes| G["Review patch and return result"] - F -->|no| H{"Use local iteration or approved Numina subagent?"} + F -->|no| H{"Use local iteration or approved Numina backend?"} H -->|yes| D - H -->|Numina| N["Call official Numina subagent after approval"] + H -->|Numina| N["Call official Numina backend after approval"] N --> E H -->|blocked| I["Extract minimal failure and report exact errors/goals"] ``` @@ -76,5 +76,5 @@ If a future agent reads this file during normal Lean work, the default action it 1. verify local Lean readiness; 2. prepare the target in the user's Lake project or shared workspace; 3. edit/check directly as a coding agent; -4. use official Numina only if the user asks for the subagent path or it is approved; +4. use official Numina only if the user asks for the supported backend path or it is approved; 5. return a verified patch or minimal failure. diff --git a/skills/lean-formalization/references/numina_runtime.md b/skills/lean-runtime/references/numina_runtime.md similarity index 71% rename from skills/lean-formalization/references/numina_runtime.md rename to skills/lean-runtime/references/numina_runtime.md index 6052384..297ff7d 100644 --- a/skills/lean-formalization/references/numina_runtime.md +++ b/skills/lean-runtime/references/numina_runtime.md @@ -1,10 +1,14 @@ -# Optional Official Numina Subagent Runtime +# Optional Official Numina Backend Adapter -This skill keeps the official `project-numina/numina-lean-agent` repository as an optional deployable subagent backend. The default path is coding-agent Lean work with local Lean/Lake validation; Numina is used when the user asks for the official Lean Agent, batch proof search, or an external subagent run. +This skill keeps the official `project-numina/numina-lean-agent` repository as the currently supported optional Lean-specialist backend adapter. The default path is coding-agent Lean work with local Lean/Lake validation; Numina is used when the user asks for the official Lean Agent, Numina, batch proof search, or an approved external subagent run. + +Currently supported optional backend: official Numina Lean Agent runtime. + +Future backend adapters may include Archon or other Lean-specialist systems, but do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented. See `backend_adapter_checklist.md` before describing any future backend as supported. ## Agent Flow -1. Clarify the target: configure Numina, call Numina on a Lean project/file/folder, validate Numina output, or continue with the default coding-agent path. +1. Clarify the target: configure the supported official Numina adapter, call Numina on a Lean project/file/folder, validate Numina output, or continue with the default coding-agent path. 2. Run `doctor --cwd .` when useful and read the `numina` readiness block before recommending a path. 3. Explain what setup may do: clone the official repository, run `tutorial/setup.sh`, install or use `elan`, `lake`, `curl`, `uv`, and `claude`, and require model/API credentials or Claude CLI auth for calls. 4. After approval, run `configure --cwd . --setup-numina --project-name `. Use `--dry-run` first when the user wants to review commands. @@ -26,7 +30,7 @@ Do not commit runtime state, API keys, generated results, or local machine paths Claude authentication can come from the user's normal Claude CLI login or environment variables such as `ANTHROPIC_AUTH_TOKEN`, `ANTHROPIC_BASE_URL`, and `ANTHROPIC_MODEL`. Numina's CLI skills may also need `GEMINI_API_KEY`, `OPENAI_API_KEY`, `LEAN_LEANDEX_API_KEY`, or `AXLE_API_KEY`. -If the user asks whether API keys are needed, distinguish the two paths: the default coding-agent Lean workflow and local Lean validation do not need API keys; official Numina subagent calls need a working Claude CLI/auth path and may need additional keys for search/tool skills. +If the user asks whether API keys are needed, distinguish the two paths: the default coding-agent Lean workflow and local Lean validation do not need API keys; official Numina backend calls need a working Claude CLI/auth path and may need additional keys for search/tool skills. The helper readiness report redacts values and only reports whether keys appear configured. diff --git a/skills/lean-formalization/references/numina_subagent_troubleshooting.md b/skills/lean-runtime/references/numina_subagent_troubleshooting.md similarity index 100% rename from skills/lean-formalization/references/numina_subagent_troubleshooting.md rename to skills/lean-runtime/references/numina_subagent_troubleshooting.md diff --git a/skills/lean-formalization/references/review_checklist.md b/skills/lean-runtime/references/review_checklist.md similarity index 100% rename from skills/lean-formalization/references/review_checklist.md rename to skills/lean-runtime/references/review_checklist.md diff --git a/skills/lean-formalization/references/specialist_agent_patterns.md b/skills/lean-runtime/references/specialist_agent_patterns.md similarity index 85% rename from skills/lean-formalization/references/specialist_agent_patterns.md rename to skills/lean-runtime/references/specialist_agent_patterns.md index 8f01667..40e4765 100644 --- a/skills/lean-formalization/references/specialist_agent_patterns.md +++ b/skills/lean-runtime/references/specialist_agent_patterns.md @@ -29,7 +29,7 @@ Public source anchors: 5. Use bounded search: try a small number of plausible tactic/proof routes; record failed routes so the agent does not cycle. 6. Retrieve before inventing: search existing project/mathlib names and nearby proofs before adding helper lemmas. 7. Validate as oracle: Lean/Lake success is required; final patches must not contain `sorry`, `admit`, new `axiom`, or unapproved statement drift. -8. Escalate deliberately: call optional Numina or another specialist backend only after explaining target, credentials/proxy/MCP state, result directory, and validation plan. +8. Escalate deliberately: call the supported official Numina adapter, or a future backend adapter only after that adapter has an explicit contract and validation gates, and only after explaining target, credentials/proxy/MCP state, result directory, and validation plan. 9. Hand off minimally: when blocked, return the smallest failing Lean fragment, exact goals/errors, tried routes, and the next mathematical decision. ## Pattern Map @@ -41,7 +41,7 @@ Public source anchors: | Premise retrieval | `rg`, nearby imports/proofs, project declarations, optional external search | | Bounded proof attempts | `max_rounds`, local iteration caps, failed-strategy notes | | Backtracking/failure memory | Record tried tactic families and rejected statement changes | -| External proof backend | Optional official Numina subagent, never required for default work | +| Lean-specialist backend adapter | Optional official Numina adapter is supported; Archon and other backends are future adapters, never required for default work | | Validation oracle | Lean/Lake plus `review` and `detect-sorry` | | Failure artifact | `minimize-failure` and exact errors/goals | @@ -49,7 +49,7 @@ Public source anchors: Default to integrated local patterns. Escalate to a real specialist backend only when: -- the user asks for Numina, official Lean Agent, batch proof search, or an external subagent; +- the user asks for Numina, official Lean Agent, batch proof search, or an approved external subagent; - local bounded attempts are cycling and the user approves a backend call; - the required credentials, proxy, MCP scope, and target project are understood; - all backend output will still be reviewed and checked locally. @@ -57,7 +57,8 @@ Default to integrated local patterns. Escalate to a real specialist backend only ## Anti-Patterns - Do not replace proof work with a CLI workflow that only asks the user for more input. -- Do not treat a missing Numina key as blocking ordinary coding-agent Lean work. +- Do not treat a missing Numina key or backend adapter as blocking ordinary coding-agent Lean work. - Do not copy upstream prompts or claim hidden benchmark behavior. - Do not add helper lemmas or theorem statement changes just to make a proof easier unless the user approves. - Do not let an external backend output bypass local Lean validation and patch review. +- Do not claim support for a backend adapter unless its setup, call, credential, mutation, and validation contracts are documented. diff --git a/skills/lean-formalization/schemas/config.schema.json b/skills/lean-runtime/schemas/config.schema.json similarity index 100% rename from skills/lean-formalization/schemas/config.schema.json rename to skills/lean-runtime/schemas/config.schema.json diff --git a/skills/lean-formalization/schemas/result.schema.json b/skills/lean-runtime/schemas/result.schema.json similarity index 100% rename from skills/lean-formalization/schemas/result.schema.json rename to skills/lean-runtime/schemas/result.schema.json diff --git a/skills/lean-formalization/schemas/task.schema.json b/skills/lean-runtime/schemas/task.schema.json similarity index 100% rename from skills/lean-formalization/schemas/task.schema.json rename to skills/lean-runtime/schemas/task.schema.json diff --git a/skills/lean-formalization/scripts/ai4m_lean.py b/skills/lean-runtime/scripts/ai4m_lean.py similarity index 98% rename from skills/lean-formalization/scripts/ai4m_lean.py rename to skills/lean-runtime/scripts/ai4m_lean.py index e7cae6f..95e96ee 100644 --- a/skills/lean-formalization/scripts/ai4m_lean.py +++ b/skills/lean-runtime/scripts/ai4m_lean.py @@ -52,10 +52,10 @@ def add_common(parser: argparse.ArgumentParser) -> None: def build_parser() -> argparse.ArgumentParser: - parser = argparse.ArgumentParser(description="AI4Math coding-agent Lean skill CLI with optional Numina subagent orchestration") + parser = argparse.ArgumentParser(description="AI4Math coding-agent Lean skill CLI with optional Lean-specialist backend adapter support") sub = parser.add_subparsers(dest="command", required=True) - env = sub.add_parser("env", help="Inspect Lean workspace and optional Numina subagent environment") + env = sub.add_parser("env", help="Inspect Lean workspace and supported optional backend environment") add_common(env) env.add_argument("--target", default=None) diff --git a/skills/lean-formalization/scripts/check_lean_project.py b/skills/lean-runtime/scripts/check_lean_project.py similarity index 100% rename from skills/lean-formalization/scripts/check_lean_project.py rename to skills/lean-runtime/scripts/check_lean_project.py diff --git a/skills/lean-formalization/scripts/common.py b/skills/lean-runtime/scripts/common.py similarity index 100% rename from skills/lean-formalization/scripts/common.py rename to skills/lean-runtime/scripts/common.py diff --git a/skills/lean-formalization/scripts/configure_lean.py b/skills/lean-runtime/scripts/configure_lean.py similarity index 99% rename from skills/lean-formalization/scripts/configure_lean.py rename to skills/lean-runtime/scripts/configure_lean.py index 1da0918..badd59e 100644 --- a/skills/lean-formalization/scripts/configure_lean.py +++ b/skills/lean-runtime/scripts/configure_lean.py @@ -75,7 +75,7 @@ def inspect_environment(cwd: str | Path = ".", config_path: str | Path | None = "mode": "coding-agent", "backend": "none", "numina_required": False, - "numina_runtime": "optional-subagent-backend", + "numina_runtime": "supported-optional-backend-adapter", }, "lean": { "target": str(target_path), diff --git a/skills/lean-formalization/scripts/detect_sorry.py b/skills/lean-runtime/scripts/detect_sorry.py similarity index 100% rename from skills/lean-formalization/scripts/detect_sorry.py rename to skills/lean-runtime/scripts/detect_sorry.py diff --git a/skills/lean-formalization/scripts/direct_task.py b/skills/lean-runtime/scripts/direct_task.py similarity index 98% rename from skills/lean-formalization/scripts/direct_task.py rename to skills/lean-runtime/scripts/direct_task.py index 26dcc9e..754ab71 100644 --- a/skills/lean-formalization/scripts/direct_task.py +++ b/skills/lean-runtime/scripts/direct_task.py @@ -79,7 +79,7 @@ def build_direct_task( "max_rounds": max_rounds, "missing_config": missing, "required_inputs": ["existing Lake project or shared reusable managed workspace"] if "lean_workspace" in missing else [], - "recommended_next_action": "run configure --create-workspace for the shared workspace or move target into a Lake project" if missing else "coding agent should edit/check directly; use Numina only if the optional subagent path is approved", + "recommended_next_action": "run configure --create-workspace for the shared workspace or move target into a Lake project" if missing else "coding agent should edit/check directly; use Numina only if the supported optional backend path is approved", "direct_workflow": next_actions, } diff --git a/skills/lean-formalization/scripts/extract_minimal_failure.py b/skills/lean-runtime/scripts/extract_minimal_failure.py similarity index 100% rename from skills/lean-formalization/scripts/extract_minimal_failure.py rename to skills/lean-runtime/scripts/extract_minimal_failure.py diff --git a/skills/lean-formalization/scripts/numina_runtime.py b/skills/lean-runtime/scripts/numina_runtime.py similarity index 100% rename from skills/lean-formalization/scripts/numina_runtime.py rename to skills/lean-runtime/scripts/numina_runtime.py diff --git a/skills/lean-formalization/scripts/smoke_test.py b/skills/lean-runtime/scripts/smoke_test.py similarity index 94% rename from skills/lean-formalization/scripts/smoke_test.py rename to skills/lean-runtime/scripts/smoke_test.py index be7720b..d36a005 100644 --- a/skills/lean-formalization/scripts/smoke_test.py +++ b/skills/lean-runtime/scripts/smoke_test.py @@ -39,7 +39,7 @@ def run_smoke_test( "ai4math_numina_smoke_le_succ", ], "external_api_call": False, - "recommended_next_action": "run the bundled smoke target, then start the coding-agent Lean task or discuss the optional Numina subagent path", + "recommended_next_action": "run the bundled smoke target, then start the coding-agent Lean task or discuss the supported optional Numina backend path", } if not workspace_root: return { @@ -64,12 +64,12 @@ def run_smoke_test( "ai4math_numina_smoke_le_succ", ], "external_api_call": False, - "recommended_next_action": "use this verified workspace for the next coding-agent Lean task; call official Numina only if the optional subagent path is approved", + "recommended_next_action": "use this verified workspace for the next coding-agent Lean task; call official Numina only if the optional backend path is approved", } lean_result = run_command(command, cwd=workspace_root, timeout=timeout) result["lean"] = lean_result result["ok"] = bool(lean_result.get("ok")) result["status"] = "ok" if result["ok"] else "lean_smoke_failed" if not result["ok"]: - result["recommended_next_action"] = "inspect the Lean smoke error, then repair the shared workspace before any Lean task or optional Numina call" + result["recommended_next_action"] = "inspect the Lean smoke error, then repair the shared workspace before any Lean task or optional backend call" return result diff --git a/skills/lean-formalization/scripts/tool_status.py b/skills/lean-runtime/scripts/tool_status.py similarity index 95% rename from skills/lean-formalization/scripts/tool_status.py rename to skills/lean-runtime/scripts/tool_status.py index 05051f6..d0303ff 100644 --- a/skills/lean-formalization/scripts/tool_status.py +++ b/skills/lean-runtime/scripts/tool_status.py @@ -76,4 +76,4 @@ def _recommend( return "install git before using Lake projects with remote dependencies" if missing_lean: return "install Lean/elan before creating the reusable Lean workspace" - return "ready for coding-agent Lean workflow and optional Numina subagent orchestration" + return "ready for coding-agent Lean workflow and supported optional Numina backend adapter orchestration" diff --git a/skills/lean-formalization/scripts/validate_patch.py b/skills/lean-runtime/scripts/validate_patch.py similarity index 100% rename from skills/lean-formalization/scripts/validate_patch.py rename to skills/lean-runtime/scripts/validate_patch.py diff --git a/skills/lean-formalization/scripts/verify_delivery.py b/skills/lean-runtime/scripts/verify_delivery.py similarity index 79% rename from skills/lean-formalization/scripts/verify_delivery.py rename to skills/lean-runtime/scripts/verify_delivery.py index cf8f04a..fe65ff4 100644 --- a/skills/lean-formalization/scripts/verify_delivery.py +++ b/skills/lean-runtime/scripts/verify_delivery.py @@ -17,11 +17,15 @@ from validate_patch import review_files -SKILL_ROOT = Path(__file__).resolve().parents[1] -SKILLS_ROOT = SKILL_ROOT.parent -REQUIRED_FILES = [ +RUNTIME_ROOT = Path(__file__).resolve().parents[1] +SKILLS_ROOT = RUNTIME_ROOT.parent +FORMALIZATION_ROOT = SKILLS_ROOT / "lean-formalization" +SETUP_ROOT = SKILLS_ROOT / "lean-setup" +REQUIRED_FORMALIZATION_FILES = [ "SKILL.md", "agents/openai.yaml", +] +REQUIRED_RUNTIME_FILES = [ "config/lean_agent.example.toml", "config/numina_runtime.example.toml", "examples/smoke/NuminaSmoke.lean", @@ -29,6 +33,7 @@ "schemas/result.schema.json", "schemas/config.schema.json", "references/lean_runtime_configuration.md", + "references/backend_adapter_checklist.md", "references/interactive_orchestration.md", "references/direct_lean_workflow.md", "references/specialist_agent_patterns.md", @@ -78,10 +83,10 @@ def _load_schema(path: Path) -> dict[str, Any]: def _package_hygiene() -> dict[str, Any]: - package_roots = [SKILL_ROOT] - setup_root = SKILLS_ROOT / "lean-setup" - if setup_root.exists(): - package_roots.append(setup_root) + package_roots = [RUNTIME_ROOT] + for root in (FORMALIZATION_ROOT, SETUP_ROOT): + if root.exists(): + package_roots.append(root) generated = [ str(path.relative_to(SKILLS_ROOT)) for root in package_roots @@ -115,31 +120,39 @@ def _package_hygiene() -> dict[str, Any]: def _guidance_first_check() -> dict[str, Any]: - text = (SKILL_ROOT / "SKILL.md").read_text(encoding="utf-8", errors="replace") - orchestration = (SKILL_ROOT / "references" / "interactive_orchestration.md").read_text(encoding="utf-8", errors="replace") + text = (FORMALIZATION_ROOT / "SKILL.md").read_text(encoding="utf-8", errors="replace") + orchestration = (RUNTIME_ROOT / "references" / "interactive_orchestration.md").read_text(encoding="utf-8", errors="replace") required_phrases = [ "## Agent Playbook", "## Helper Toolbox", "This is a coding-agent-first Lean skill.", "The coding agent is the primary Lean worker.", - "Official Numina is an optional deployable subagent backend.", + "Lean-specialist backend adapters are optional escalation paths.", + "optional Lean-specialist backend", + "Currently supported optional backend: official Numina Lean Agent runtime", + "Official Numina is the only currently supported deployable backend adapter", + "Archon and other backends are future adapters", + "future adapters until an adapter contract, setup path, call path, and local validation gates are implemented", + "do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented", + "Default coding-agent Lean work must not require any backend adapter.", + "Use the official Numina adapter only when the user asks for the official Lean Agent, Numina, batch proof search, or an approved external subagent run.", "Default execution mode is coding-agent mode.", "Incorporate publicly documented Lean-specialist agent patterns into the default coding-agent workflow.", "Treat specialist-agent patterns as mechanisms, not mandatory external services.", - "Use Numina when the user asks for the official Lean Agent, batch proof search, or an external subagent run.", "Use the bundled smoke test when no user target is available.", "Lead the interaction; do not wait for the user to drive every step.", "If the user's language is ambiguous, default to Chinese.", "A language switch is not a task reset.", "If no target is available, run or propose a safe local smoke/readiness check.", "Avoid ending with only \"send me a file\"", - "Opening readiness should inspect local Lean readiness and Numina subagent readiness separately.", + "Opening readiness should inspect local Lean readiness first", + "inspect Numina or another backend readiness only when the user asks for an optional Lean-specialist 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.", "offer a small next-step menu", "Ask at most one blocking question at a time.", "The bundled CLI is a helper toolbox, not the workflow driver.", - "Use official Numina through a human-in-the-loop subagent workflow.", + "Use official Numina through a human-in-the-loop backend adapter workflow.", "Do not turn helper commands into a closed proof workflow.", "Do not remove the official Numina subagent path.", ] @@ -147,26 +160,31 @@ def _guidance_first_check() -> dict[str, Any]: orchestration_required = [ "## Session Opening", "This is a coding-agent-first Lean skill.", - "Official Numina is an optional deployable subagent backend.", + "Official Numina is the only currently supported deployable backend adapter", + "Archon and other backends are future adapters", "The default coding-agent path should still absorb Lean-specialist agent mechanisms:", "Use the bundled smoke test when no user target is available.", "Lead the interaction; do not wait for the user to drive every step.", "A language switch is not a task reset.", "If no target is available, run or propose a safe local smoke/readiness check.", "Avoid ending with only \"send me a file\"", - "Opening readiness should inspect local Lean readiness and Numina subagent readiness separately.", + "Opening readiness should inspect local Lean readiness first", + "Inspect Numina or another backend readiness only when the user asks for an optional Lean-specialist 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.", "A good opening ends with one decision question, not a checklist.", ] orchestration_missing = [phrase for phrase in orchestration_required if phrase not in orchestration] - openai_yaml = (SKILL_ROOT / "agents" / "openai.yaml").read_text(encoding="utf-8", errors="replace") + openai_yaml = (FORMALIZATION_ROOT / "agents" / "openai.yaml").read_text(encoding="utf-8", errors="replace") openai_required = [ "请用中文开始", "如果用户明确使用其他语言", "默认走 coding agent Lean 工作流", "该 skill 参考并整合", - "Numina 是可部署的可选 subagent", + "目前只承诺 official Numina adapter 已支持", + "Archon 和其他 backend 只能作为 future adapters", + "默认开场检查本地 Lean/shared workspace readiness", + "仅当用户要求 optional backend 时再检查 Numina readiness", ] openai_missing = [phrase for phrase in openai_required if phrase not in openai_yaml] return { @@ -209,16 +227,14 @@ def _root_discovery_boundary_check() -> dict[str, Any]: def _lean_setup_entrypoint_check() -> dict[str, Any]: - setup_root = SKILLS_ROOT / "lean-setup" - readme_path = setup_root / "README.md" - skill_path = setup_root / "SKILL.md" - openai_path = setup_root / "agents" / "openai.yaml" - helper_script = SKILL_ROOT / "scripts" / "ai4m_lean.py" - required_files = [readme_path, skill_path, openai_path] + skill_path = SETUP_ROOT / "SKILL.md" + openai_path = SETUP_ROOT / "agents" / "openai.yaml" + helper_script = RUNTIME_ROOT / "scripts" / "ai4m_lean.py" + required_files = [skill_path, openai_path] if not all(path.exists() for path in required_files): return { "ok": False, - "setup_root": str(setup_root), + "setup_root": str(SETUP_ROOT), "helper_script": str(helper_script), "helper_script_exists": helper_script.exists(), "missing_files": [str(path) for path in required_files if not path.exists()], @@ -231,24 +247,31 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]: required_phrases = [ "Use this setup-only entrypoint", "Do not ask for a theorem target in setup-only mode.", - "The canonical implementation lives in `../lean-formalization/`.", - "../lean-formalization/scripts/ai4m_lean.py", + "The shared implementation lives in `../lean-runtime/`.", + "../lean-runtime/scripts/ai4m_lean.py", "Install Lean through the official `elan` channel", "When creating an isolated test directory or workspace", "suggest a safe default name", "use the default if the user has no naming preference", + "After successful setup or smoke-test validation", + "Offer a short next-step menu", + "inspect an existing Lean/Lake project", + "repair a Lean file or complete `sorry`", + "formalize a natural-language or LaTeX theorem", + "mention optional Numina only when the user explicitly asks", "Do not require API keys for Lean/mathlib workspace setup.", "hand off to `lean-formalization`", ] repo_root_commands = [ - "python skills/lean-formalization/scripts/ai4m_lean.py", + "python skills/" + "lean-formalization/scripts/ai4m_lean.py", ] repo_root_command_hits = [phrase for phrase in repo_root_commands if phrase in text] openai_required = [ "不要向用户索要 theorem target", - "所有实现应复用 lean-formalization", + "setup 完成后主动给出下一步菜单", + "所有实现应复用 lean-runtime", "默认 Lean/mathlib 环境配置不需要 API key", - "先给出安全默认名称并允许用户确认或改名", + "不要把 Numina 放进默认下一步", "应交接到 lean-formalization", ] return { @@ -258,7 +281,7 @@ def _lean_setup_entrypoint_check() -> dict[str, Any]: and all(phrase in text for phrase in required_phrases) and all(phrase in openai_yaml for phrase in openai_required) ), - "setup_root": str(setup_root), + "setup_root": str(SETUP_ROOT), "helper_script": str(helper_script), "helper_script_exists": helper_script.exists(), "missing_phrases": [phrase for phrase in required_phrases if phrase not in text], @@ -274,18 +297,24 @@ def verify( run_tests: bool = False, ) -> dict[str, Any]: cwd_path = Path(cwd).resolve() - files = [{"path": item, "exists": (SKILL_ROOT / item).exists()} for item in REQUIRED_FILES] + files = [ + {"path": f"lean-formalization/{item}", "exists": (FORMALIZATION_ROOT / item).exists()} + for item in REQUIRED_FORMALIZATION_FILES + ] + [ + {"path": f"lean-runtime/{item}", "exists": (RUNTIME_ROOT / item).exists()} + for item in REQUIRED_RUNTIME_FILES + ] commands = _parser_commands() schemas = [] for name in ("task.schema.json", "result.schema.json", "config.schema.json"): - path = SKILL_ROOT / "schemas" / name + path = RUNTIME_ROOT / "schemas" / name try: _load_schema(path) schemas.append({"path": f"schemas/{name}", "ok": True}) except Exception as exc: # noqa: BLE001 - report schema parse failure in JSON schemas.append({"path": f"schemas/{name}", "ok": False, "error": str(exc)}) - fixtures = SKILL_ROOT / "tests" / "fixtures" + fixtures = RUNTIME_ROOT / "tests" / "fixtures" with tempfile.TemporaryDirectory() as tmp: dry_root = Path(tmp) dry_target = dry_root / "Failure.lean" @@ -313,7 +342,7 @@ def verify( tests = None if run_tests: - tests = run_command([sys.executable, "-m", "unittest", "discover", "-s", str(SKILL_ROOT / "tests")], cwd=SKILL_ROOT, timeout=300) + tests = run_command([sys.executable, "-m", "unittest", "discover", "-s", str(RUNTIME_ROOT / "tests")], cwd=RUNTIME_ROOT, timeout=300) hygiene = _package_hygiene() guidance_first = _guidance_first_check() @@ -347,7 +376,9 @@ def verify( "ok": ok, "status": "delivery_ready" if ok else "delivery_blocked", "cwd": str(cwd_path), - "skill_root": str(SKILL_ROOT), + "runtime_root": str(RUNTIME_ROOT), + "formalization_root": str(FORMALIZATION_ROOT), + "setup_root": str(SETUP_ROOT), "checks": checks, "files": files, "commands": { diff --git a/skills/lean-formalization/tests/fixtures/after_bad.lean b/skills/lean-runtime/tests/fixtures/after_bad.lean similarity index 100% rename from skills/lean-formalization/tests/fixtures/after_bad.lean rename to skills/lean-runtime/tests/fixtures/after_bad.lean diff --git a/skills/lean-formalization/tests/fixtures/after_statement_changed.lean b/skills/lean-runtime/tests/fixtures/after_statement_changed.lean similarity index 100% rename from skills/lean-formalization/tests/fixtures/after_statement_changed.lean rename to skills/lean-runtime/tests/fixtures/after_statement_changed.lean diff --git a/skills/lean-formalization/tests/fixtures/before.lean b/skills/lean-runtime/tests/fixtures/before.lean similarity index 100% rename from skills/lean-formalization/tests/fixtures/before.lean rename to skills/lean-runtime/tests/fixtures/before.lean diff --git a/skills/lean-formalization/tests/fixtures/failure.lean b/skills/lean-runtime/tests/fixtures/failure.lean similarity index 100% rename from skills/lean-formalization/tests/fixtures/failure.lean rename to skills/lean-runtime/tests/fixtures/failure.lean diff --git a/skills/lean-formalization/tests/test_check_lean_project.py b/skills/lean-runtime/tests/test_check_lean_project.py similarity index 100% rename from skills/lean-formalization/tests/test_check_lean_project.py rename to skills/lean-runtime/tests/test_check_lean_project.py diff --git a/skills/lean-formalization/tests/test_cli.py b/skills/lean-runtime/tests/test_cli.py similarity index 74% rename from skills/lean-formalization/tests/test_cli.py rename to skills/lean-runtime/tests/test_cli.py index 0780675..275a8dd 100644 --- a/skills/lean-formalization/tests/test_cli.py +++ b/skills/lean-runtime/tests/test_cli.py @@ -9,6 +9,7 @@ from pathlib import Path SKILL_ROOT = Path(__file__).resolve().parents[1] +SKILLS_ROOT = SKILL_ROOT.parent sys.path.insert(0, str(SKILL_ROOT / "scripts")) from ai4m_lean import EXIT_LEAN_FAILED, _exit_code # noqa: E402 @@ -162,12 +163,57 @@ def test_lean_setup_entrypoint_uses_sibling_helper_layout(self) -> None: self.assertTrue(setup["helper_script_exists"], setup) self.assertFalse(setup["repo_root_command_hits"], setup) + def test_two_public_skills_share_hidden_runtime_layer(self) -> None: + runtime_root = SKILLS_ROOT / "lean-runtime" + runtime_cli = runtime_root / "scripts" / "ai4m_lean.py" + setup_text = (SKILLS_ROOT / "lean-setup" / "SKILL.md").read_text(encoding="utf-8") + formalization_text = (SKILLS_ROOT / "lean-formalization" / "SKILL.md").read_text(encoding="utf-8") + + self.assertTrue(runtime_cli.exists()) + self.assertIn("../lean-runtime/scripts/ai4m_lean.py", setup_text) + self.assertIn("../lean-runtime/scripts/ai4m_lean.py", formalization_text) + self.assertNotIn("../lean-formalization/scripts/ai4m_lean.py", setup_text) + def test_lean_setup_offers_default_names_for_isolated_setup(self) -> None: text = (SKILL_ROOT.parent / "lean-setup" / "SKILL.md").read_text(encoding="utf-8") self.assertIn("When creating an isolated test directory or workspace", text) self.assertIn("suggest a safe default name", text) self.assertIn("use the default if the user has no naming preference", text) + def test_lean_setup_guides_next_step_after_successful_setup(self) -> None: + text = (SKILL_ROOT.parent / "lean-setup" / "SKILL.md").read_text(encoding="utf-8") + self.assertIn("After successful setup or smoke-test validation", text) + self.assertIn("Offer a short next-step menu", text) + self.assertIn("inspect an existing Lean/Lake project", text) + self.assertIn("repair a Lean file or complete `sorry`", text) + self.assertIn("formalize a natural-language or LaTeX theorem", text) + self.assertIn("mention optional Numina only when the user explicitly asks", text) + + def test_optional_backend_language_distinguishes_current_and_future_adapters(self) -> None: + repo_root = SKILLS_ROOT.parent + texts = [ + (SKILLS_ROOT / "lean-formalization" / "SKILL.md").read_text(encoding="utf-8"), + (SKILL_ROOT / "references" / "numina_runtime.md").read_text(encoding="utf-8"), + ] + readme_path = repo_root / "README.md" + readme_zh_path = repo_root / "README.zh-CN.md" + if readme_path.exists(): + texts.append(readme_path.read_text(encoding="utf-8")) + + for text in texts: + self.assertIn("optional Lean-specialist backend", text) + self.assertIn("Currently supported optional backend: official Numina Lean Agent runtime", text) + self.assertIn("Future backend adapters", text) + self.assertIn("do not claim support until deployment, readiness checks, invocation, validation, and failure triage are documented", text) + self.assertNotIn("Currently supported optional backend: Archon", text) + + if readme_zh_path.exists(): + readme_zh = readme_zh_path.read_text(encoding="utf-8") + self.assertIn("可选 Lean 专用 agent backend", readme_zh) + self.assertIn("当前支持的可选 backend：official Numina Lean Agent runtime", readme_zh) + self.assertIn("未来 backend adapter", readme_zh) + self.assertIn("不要写成已支持", readme_zh) + def test_package_hygiene_scans_lean_setup_entrypoint(self) -> None: generated = SKILL_ROOT.parent / "lean-setup" / "__pycache__" / "sentinel.pyc" generated.parent.mkdir(exist_ok=True) diff --git a/skills/lean-formalization/tests/test_common_config.py b/skills/lean-runtime/tests/test_common_config.py similarity index 100% rename from skills/lean-formalization/tests/test_common_config.py rename to skills/lean-runtime/tests/test_common_config.py diff --git a/skills/lean-formalization/tests/test_configure_lean.py b/skills/lean-runtime/tests/test_configure_lean.py similarity index 99% rename from skills/lean-formalization/tests/test_configure_lean.py rename to skills/lean-runtime/tests/test_configure_lean.py index 9ece591..1d5c15f 100644 --- a/skills/lean-formalization/tests/test_configure_lean.py +++ b/skills/lean-runtime/tests/test_configure_lean.py @@ -31,7 +31,7 @@ def test_existing_lean_project_is_coding_agent_ready(self) -> None: self.assertEqual(result["agent"]["mode"], "coding-agent") self.assertEqual(result["agent"]["backend"], "none") self.assertFalse(result["agent"]["numina_required"]) - self.assertEqual(result["agent"]["numina_runtime"], "optional-subagent-backend") + self.assertEqual(result["agent"]["numina_runtime"], "supported-optional-backend-adapter") self.assertEqual(result["missing_config"], []) self.assertIn("numina", result) self.assertIn("readiness", result["numina"]) diff --git a/skills/lean-formalization/tests/test_detect_sorry.py b/skills/lean-runtime/tests/test_detect_sorry.py similarity index 100% rename from skills/lean-formalization/tests/test_detect_sorry.py rename to skills/lean-runtime/tests/test_detect_sorry.py diff --git a/skills/lean-formalization/tests/test_direct_task.py b/skills/lean-runtime/tests/test_direct_task.py similarity index 100% rename from skills/lean-formalization/tests/test_direct_task.py rename to skills/lean-runtime/tests/test_direct_task.py diff --git a/skills/lean-formalization/tests/test_numina_runtime.py b/skills/lean-runtime/tests/test_numina_runtime.py similarity index 100% rename from skills/lean-formalization/tests/test_numina_runtime.py rename to skills/lean-runtime/tests/test_numina_runtime.py diff --git a/skills/lean-formalization/tests/test_validate_patch.py b/skills/lean-runtime/tests/test_validate_patch.py similarity index 100% rename from skills/lean-formalization/tests/test_validate_patch.py rename to skills/lean-runtime/tests/test_validate_patch.py diff --git a/skills/lean-setup/SKILL.md b/skills/lean-setup/SKILL.md index 26a7c97..be22520 100644 --- a/skills/lean-setup/SKILL.md +++ b/skills/lean-setup/SKILL.md @@ -7,7 +7,7 @@ description: Use when a coding agent needs to install or verify Lean 4, elan, la Use this setup-only entrypoint when the user only wants a Lean 4 environment, `elan`/`lake` readiness, or a reusable mathlib workspace. Do not ask for a theorem target in setup-only mode. -The canonical implementation lives in `../lean-formalization/`. This skill must reuse the same helper CLI, configuration rules, and runtime references rather than duplicating setup logic. +The shared implementation lives in `../lean-runtime/`. This skill must reuse the same helper CLI, configuration rules, and runtime references rather than duplicating setup logic or depending on the formalization entrypoint. ## Setup-Only Flow @@ -20,17 +20,30 @@ The canonical implementation lives in `../lean-formalization/`. This skill must 7. Create the workspace only after explaining that Lean/mathlib artifacts may be downloaded or built. 8. Run the bundled smoke test after setup. 9. Report the installed tools, workspace path, Lean toolchain, mathlib revision when available, smoke-test result, and any remaining action. -10. If the user next wants formalization, proof repair, theorem transcription, `sorry` completion, patch review, or Numina proof search, hand off to `lean-formalization`. +10. After successful setup or smoke-test validation, do not end passively. Offer a short next-step menu and recommend one default next action. +11. If the user next wants formalization, proof repair, theorem transcription, `sorry` completion, patch review, or Numina proof search, hand off to `lean-formalization`. + +## Post-Setup Guidance + +Offer a short next-step menu after setup succeeds: + +- inspect an existing Lean/Lake project; +- run or explain the built-in smoke theorem result; +- repair a Lean file or complete `sorry`; +- formalize a natural-language or LaTeX theorem; +- continue setup-only validation if the user only wants environment readiness. + +As a rule, mention optional Numina only when the user explicitly asks for the official Lean Agent, batch proof search, or an external backend adapter; do not make Numina or API keys part of the default next step. ## Commands -Resolve the helper from the sibling skill path `../lean-formalization/scripts/ai4m_lean.py`, then run it with `--cwd `. In a source checkout this is the same helper under `skills/lean-formalization/scripts/ai4m_lean.py`. +Resolve the helper from the shared runtime path `../lean-runtime/scripts/ai4m_lean.py`, then run it with `--cwd `. In a source checkout this is the same helper under `skills/lean-runtime/scripts/ai4m_lean.py`. ```bash -python ../lean-formalization/scripts/ai4m_lean.py doctor --cwd -python ../lean-formalization/scripts/ai4m_lean.py env --cwd -python ../lean-formalization/scripts/ai4m_lean.py configure --cwd --create-workspace -python ../lean-formalization/scripts/ai4m_lean.py smoke-test --cwd +python ../lean-runtime/scripts/ai4m_lean.py doctor --cwd +python ../lean-runtime/scripts/ai4m_lean.py env --cwd +python ../lean-runtime/scripts/ai4m_lean.py configure --cwd --create-workspace +python ../lean-runtime/scripts/ai4m_lean.py smoke-test --cwd ``` Use `--dry-run` before setup when the user wants to review commands. @@ -45,6 +58,6 @@ Use `--dry-run` before setup when the user wants to review commands. ## References -- Read `../lean-formalization/references/lean_runtime_configuration.md` for shared workspace layout, local configuration, and version policy. -- Read `../lean-formalization/references/numina_runtime.md` only when the user asks for optional official Numina setup. -- Use `../lean-formalization/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests` for package validation. +- Read `../lean-runtime/references/lean_runtime_configuration.md` for shared workspace layout, local configuration, and version policy. +- Read `../lean-runtime/references/numina_runtime.md` only when the user asks for optional official Numina setup. +- Use `../lean-runtime/scripts/ai4m_lean.py verify-delivery --cwd . --run-tests` for package validation. diff --git a/skills/lean-setup/agents/openai.yaml b/skills/lean-setup/agents/openai.yaml index bdf9f58..81dee2e 100644 --- a/skills/lean-setup/agents/openai.yaml +++ b/skills/lean-setup/agents/openai.yaml @@ -1,3 +1,3 @@ display_name: Lean Setup short_description: Lean 4, elan, lake, and reusable mathlib workspace setup for coding agents. -default_prompt: 请默认使用中文，并主动完成 Lean 环境配置引导；仅当用户明确使用其他语言时切换。该入口仅用于 setup-only 任务：检查或安装 Lean/elan/lake，创建或复用带 mathlib 的共享工作区，运行 smoke-test，并报告 workspace 路径、toolchain、mathlib revision、验证结果与剩余动作。创建隔离测试目录或 workspace 时，先给出安全默认名称并允许用户确认或改名；用户无偏好时使用默认名称。不要向用户索要 theorem target。所有实现应复用 lean-formalization 的 helper CLI 与 runtime references，不复制第二套配置逻辑。默认 Lean/mathlib 环境配置不需要 API key；只有在用户明确要求 optional official Numina backend 时，才说明凭据需求并请求批准。配置完成后，如用户要进行形式化、proof repair、sorry completion 或 Numina proof search，应交接到 lean-formalization。 +default_prompt: 请默认使用中文，并主动完成 Lean 环境配置引导；仅当用户明确使用其他语言时切换。该入口仅用于 setup-only 任务：检查或安装 Lean/elan/lake，创建或复用带 mathlib 的共享工作区，运行 smoke-test，并报告 workspace 路径、toolchain、mathlib revision、验证结果与剩余动作。不要向用户索要 theorem target。setup 完成后主动给出下一步菜单，例如检查 Lean/Lake 项目、运行或解释 smoke theorem、修 Lean 文件或补 sorry、形式化自然语言/LaTeX 命题，或继续 setup-only readiness；推荐一个默认下一步。所有实现应复用 lean-runtime 的 helper CLI 与 runtime references，不复制第二套配置逻辑，也不要把 lean-formalization 当作 setup 的实现依赖。默认 Lean/mathlib 环境配置不需要 API key；只有在用户明确要求 optional official Numina backend 时，才说明凭据需求并请求批准，不要把 Numina 放进默认下一步。配置完成后，如用户要进行形式化、proof repair、sorry completion 或 Numina proof search，应交接到 lean-formalization。