VeryMath · ConanXu-math · Jun 26, 2026 · May 22, 2026 · May 22, 2026 · May 24, 2026
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -12,17 +12,23 @@ 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.
 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.
 
-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
@@ -12,17 +12,17 @@ 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.
 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.
 
-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
@@ -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,19 +75,21 @@ 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
 
 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
@@ -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,15 +16,21 @@
 
 这个仓库是 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 合约文档化后再宣称支持；不要写成已支持。
+
 ## 技能包
 
 | 包 | 适用任务 | 入口 |
 | --- | --- | --- |
 | [`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 链接。