Lean Research Library
Steward for the user's personal mathlib-style staging library
(HoangMathLib) and paper-artifact template. Propose-only by design: this
skill never commits, pushes, opens PRs, or publishes — those remain user
actions behind explicit approval gates.
Hard contract (applies on every install target)
- Before any Lean formalization — whatever skill, plugin, template, or
agent lane starts it — run
search for each target statement. Precedence
is normative: mathlib hit → use mathlib, stop; else library hit → use the
library; else peer-satellite hit → cite it and decide; else formalize
new. A statement_only hit (e.g. FormalConjectures) is a sorry'd
statement, never a reusable proof.
- After a formalization result is accepted — run
intake on the new
file. A declaration is a library candidate only if it is (i) absent
from mathlib AND the library (search-verified) and (ii) useful beyond the
immediate task; everything else stays where it was produced. Present the
proposal packet with a usefulness justification per candidate and ask
before any stage --apply. Never write to the library without that
approval. For paper-artifact campaigns, this intake pass runs once,
after the full formalization is complete, not per result.
- Two actions are always user-gated, even inside autonomous loops:
staging into the library, and anything outward-facing (repo creation,
pushes, Zenodo publishing). Autonomous runs batch these gates at run
boundaries; nothing is auto-published mid-loop.
Configuration
Resolution order: AAS_LEAN_LIBRARY_ROOT env var → config file
(${XDG_CONFIG_HOME:-~/.config}/lean-research-library/config.json; on
Windows %APPDATA%\lean-research-library\config.json). Keys:
library_root, library_module (default HoangMathLib), template_root
(clone of lean-paper-artifact-template), peer_satellites (list of local
checkout paths, e.g. cam-combi, add-combi), closed_deps (bool: restrict to
Lean core + mathlib + the library; disables the peer-satellite tier — use
for closed-dependency formalization pipelines).
Run doctor on a fresh machine: it prints exact clone commands and the
config to write (first-run bootstrap). Missing Lean is a reported status,
never a failure; the skill installs nothing.
Verbs
| Verb |
Network |
Purpose |
doctor [--ecosystem] |
no / marked |
Tools, config, first-run bootstrap; --ecosystem re-checks latest stable mathlib vs pin and search-endpoint liveness (drift detection). |
search --query Q [--offline] [--with-leansearch] |
marked |
Bucketed reuse check: {mathlib, library, peer_satellite, elsewhere} + recommendation per the precedence rule. Backends: library grep + decls-index.jsonl, peer-satellite greps, Loogle (with quoted-form retry), LeanStateSearch; LeanSearch off by default. Endpoints env-overridable (AAS_LOOGLE_URL, …) — pointing AAS_LOOGLE_URL at a self-hosted loogle (server.py --project-dir <library>) gives type-pattern search over the personal library itself. |
status |
no |
Library pin, staging readiness (sorry-free + import discipline per file), research sorry census. |
intake --file F |
no |
The ask-the-user gate: proposal packet per declaration + a lean-strict-verification-gate packet (typechecking ≠ claim support). Writes nothing. |
stage --file F --target T [--apply] |
no |
Dry-run by default. Two targets: Mathlib/A/B/C.lean (staging mirror; validates sorry-freedom, import discipline, pinned-mathlib file form, offers header scaffold) or research dirs (e.g. Reconfig/X.lean). --apply only after user approval; commits stay with the user. |
prepare-upstream --file F |
no |
Port-to-master packet: rewritten imports (<Lib>.Mathlib.X → Mathlib.X), mathlib PR checklist (header form, fix_deprecations, title conventions, AI disclosure). |
bump [--to TAG] [--apply] |
marked |
Stable-ladder bump: dry-run shows the ladder + checklist; --apply edits lean-toolchain + lakefile rev only, then hands the lake commands to the user. |
audit [--run-gate] |
no |
Staging violations + the deterministic landed-in-mathlib gate. Default prints the exact commands; --run-gate executes them when lake and a built library are available (minutes; imports the full mathlib closure). Nonzero gate exit = delete or rename the staged copy. |
artifact new --paper SLUG --dir D [--library-rev SHA] |
no |
Scaffold from template_root (full verification ladder) or an embedded minimal fallback; proposes — never runs — gh repo create/push and the per-paper library tag. |
artifact publish --dir D [--mode github-sync|api] |
marked |
Zenodo: github-sync prints the verified checklist; api targets sandbox by default, needs ZENODO_TOKEN, and refuses --production without --confirm-production (a published DOI cannot be deleted). Prechecks block on leftover <PLACEHOLDER>s. Uploads/publish stay gated. |
Paper→formalization pipeline (with autonomous-research-loop)
For "formalize this paper end to end": intake the paper's claims
(lean-formalization-intake), skeleton statements
(formal-skeleton-helper), then drive proof work with
autonomous-research-loop using formal_policy: force and this skill wired
at F2′ (search-first) and F7′ (intake-after). Set closed_deps: true for a
core+mathlib+library-only run. The loop ends in exactly one of two states:
a sorry-free artifact scaffolded by artifact new, or an honest ledger of
open statements — lean-strict-verification-gate decides which, never the
loop itself. Heavy proof iteration needs a mathlib toolchain: run where one
exists or route through the compute-lane skills.
Windows Runtime Commands
Runtime helpers live under the shared runtime root. From PowerShell:
$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }
& "$runtime\run_skill.ps1" "skills/lean-research-library/run_lean_research_library.ps1" doctor
or directly from PowerShell: skills/lean-research-library/run_lean_research_library.ps1
and skills/lean-research-library/run_lean_research_library.ps1 (both
resolve Python via run_python.ps1/AAS_RUNTIME_PYTHON). On POSIX:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" skills/lean-research-library/run_lean_research_library.sh doctor
Recommended templates
informal-to-lean-formalization-runbook — the F1–F7 formal lane this
skill's F2′/F7′ gates extend.
1---2name: lean-research-library3description: Use when any Lean formalization task starts (reuse Mathlib and the personal research library before proving anything new) and when it ends (gate finished results into the library and flag mathlib-PR candidates, always asking the user first). Also scaffolds and publishes paper artifacts from the personal template.4---56# Lean Research Library78Steward for the user's personal mathlib-style staging library9(`HoangMathLib`) and paper-artifact template. Propose-only by design: this10skill never commits, pushes, opens PRs, or publishes — those remain user11actions behind explicit approval gates.1213## Hard contract (applies on every install target)14151. **Before any Lean formalization** — whatever skill, plugin, template, or16 agent lane starts it — run `search` for each target statement. Precedence17 is normative: **mathlib hit → use mathlib, stop; else library hit → use the18 library; else peer-satellite hit → cite it and decide; else formalize19 new.** A `statement_only` hit (e.g. FormalConjectures) is a sorry'd20 statement, never a reusable proof.212. **After a formalization result is accepted** — run `intake` on the new22 file. A declaration is a library candidate **only if** it is (i) absent23 from mathlib AND the library (search-verified) and (ii) useful beyond the24 immediate task; everything else stays where it was produced. Present the25 proposal packet with a usefulness justification per candidate and **ask26 before any `stage --apply`**. Never write to the library without that27 approval. For paper-artifact campaigns, this intake pass runs **once,28 after the full formalization is complete**, not per result.293. **Two actions are always user-gated**, even inside autonomous loops:30 staging into the library, and anything outward-facing (repo creation,31 pushes, Zenodo publishing). Autonomous runs batch these gates at run32 boundaries; nothing is auto-published mid-loop.3334## Configuration3536Resolution order: `AAS_LEAN_LIBRARY_ROOT` env var → config file37(`${XDG_CONFIG_HOME:-~/.config}/lean-research-library/config.json`; on38Windows `%APPDATA%\lean-research-library\config.json`). Keys:39`library_root`, `library_module` (default `HoangMathLib`), `template_root`40(clone of `lean-paper-artifact-template`), `peer_satellites` (list of local41checkout paths, e.g. cam-combi, add-combi), `closed_deps` (bool: restrict to42Lean core + mathlib + the library; disables the peer-satellite tier — use43for closed-dependency formalization pipelines).4445Run `doctor` on a fresh machine: it prints exact clone commands and the46config to write (first-run bootstrap). Missing Lean is a reported status,47never a failure; the skill installs nothing.4849## Verbs5051| Verb | Network | Purpose |52|---|---|---|53| `doctor [--ecosystem]` | no / marked | Tools, config, first-run bootstrap; `--ecosystem` re-checks latest stable mathlib vs pin and search-endpoint liveness (drift detection). |54| `search --query Q [--offline] [--with-leansearch]` | marked | Bucketed reuse check: `{mathlib, library, peer_satellite, elsewhere}` + recommendation per the precedence rule. Backends: library grep + `decls-index.jsonl`, peer-satellite greps, Loogle (with quoted-form retry), LeanStateSearch; LeanSearch off by default. Endpoints env-overridable (`AAS_LOOGLE_URL`, …) — pointing `AAS_LOOGLE_URL` at a self-hosted loogle (`server.py --project-dir <library>`) gives type-pattern search over the personal library itself. |55| `status` | no | Library pin, staging readiness (sorry-free + import discipline per file), research sorry census. |56| `intake --file F` | no | The ask-the-user gate: proposal packet per declaration + a lean-strict-verification-gate packet (typechecking ≠ claim support). Writes nothing. |57| `stage --file F --target T [--apply]` | no | Dry-run by default. Two targets: `Mathlib/A/B/C.lean` (staging mirror; validates sorry-freedom, import discipline, pinned-mathlib file form, offers header scaffold) or research dirs (e.g. `Reconfig/X.lean`). `--apply` only after user approval; commits stay with the user. |58| `prepare-upstream --file F` | no | Port-to-master packet: rewritten imports (`<Lib>.Mathlib.X → Mathlib.X`), mathlib PR checklist (header form, fix_deprecations, title conventions, AI disclosure). |59| `bump [--to TAG] [--apply]` | marked | Stable-ladder bump: dry-run shows the ladder + checklist; `--apply` edits `lean-toolchain` + lakefile rev only, then hands the lake commands to the user. |60| `audit [--run-gate]` | no | Staging violations + the deterministic landed-in-mathlib gate. Default prints the exact commands; `--run-gate` executes them when lake and a built library are available (minutes; imports the full mathlib closure). Nonzero gate exit = delete or rename the staged copy. |61| `artifact new --paper SLUG --dir D [--library-rev SHA]` | no | Scaffold from `template_root` (full verification ladder) or an embedded minimal fallback; proposes — never runs — `gh repo create`/push and the per-paper library tag. |62| `artifact publish --dir D [--mode github-sync\|api]` | marked | Zenodo: `github-sync` prints the verified checklist; `api` targets **sandbox by default**, needs `ZENODO_TOKEN`, and **refuses `--production` without `--confirm-production`** (a published DOI cannot be deleted). Prechecks block on leftover `<PLACEHOLDER>`s. Uploads/publish stay gated. |6364## Paper→formalization pipeline (with autonomous-research-loop)6566For "formalize this paper end to end": intake the paper's claims67(`lean-formalization-intake`), skeleton statements68(`formal-skeleton-helper`), then drive proof work with69`autonomous-research-loop` using `formal_policy: force` and this skill wired70at F2′ (search-first) and F7′ (intake-after). Set `closed_deps: true` for a71core+mathlib+library-only run. The loop ends in exactly one of two states:72a sorry-free artifact scaffolded by `artifact new`, or an honest ledger of73open statements — `lean-strict-verification-gate` decides which, never the74loop itself. Heavy proof iteration needs a mathlib toolchain: run where one75exists or route through the compute-lane skills.7677## Windows Runtime Commands7879Runtime helpers live under the shared runtime root. From PowerShell:8081```powershell82$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }83& "$runtime\run_skill.ps1" "skills/lean-research-library/run_lean_research_library.ps1" doctor84```8586or directly from PowerShell: `skills/lean-research-library/run_lean_research_library.ps1`87and `skills/lean-research-library/run_lean_research_library.ps1` (both88resolve Python via `run_python.ps1`/`AAS_RUNTIME_PYTHON`). On POSIX:8990```bash91bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" skills/lean-research-library/run_lean_research_library.sh doctor92```9394## Recommended templates9596- `informal-to-lean-formalization-runbook` — the F1–F7 formal lane this97 skill's F2′/F7′ gates extend.
hoanganhduc