القائمة
Use when checking whether a Lean artifact can safely support a research claim.
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
استنادا إلى تصنيف SOC المهني
Use when the user asks for a multi-agent discussion, panel review, multi-agent review, or multi-agent research session with role selection, round control, and template-based orchestration.
Use when drafting, validating, or normalizing bounded cross-agent task/result packets for parent-controlled handoffs. This is a packet-contract skill, not a runtime delegation broker.
Send email over SMTP using only the Python standard library, with plain-text and HTML bodies, file attachments, cc/bcc, reply-to, a dry-run preview, connection verification, and redacted config inspection.
Runtime helper for autonomous-research-loop ledgers. Use to initialize, append, validate, inspect, or smoke-test autonomous research loop state files without network, package installation, provider CLI calls, or live agent spawning.
Run bounded autonomous research iterations with evidence gates, recovery ledgers, and optional cross-agent handoffs. Use when the user asks to continue research autonomously, run a research loop, integrate autonomous agent loops, or keep improving a research workflow without repeated prompts.
Use for external DOI/ISBN/title resolution, manifest creation from pasted text, and paper retrieval after the local library-first workflow does not satisfy the request or the user explicitly opts out of library use.
| name | lean-strict-verification-gate |
| description | Use when checking whether a Lean artifact can safely support a research claim. |
On native Windows, use the managed Windows runner and the native runtime command target. Set $runtime to the installed runtime root. Multi-agent installs usually use %LOCALAPPDATA%\ai-agents-skills\runtime. Then run:
$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }
& "$runtime\run_skill.bat" "skills/lean-strict-verification-gate/run_lean_strict_verification_gate.bat" doctor
PowerShell runner target:
& "$runtime\run_skill.ps1" "skills/lean-strict-verification-gate/run_lean_strict_verification_gate.ps1" doctor
POSIX examples below use run_skill.sh and .sh command targets; use the Windows command target above on native Windows.
Use this skill to prevent overclaiming from generated Lean, skeletons, partial formalizations, or checker output. It separates:
Check the local tool status:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-strict-verification-gate/run_lean_strict_verification_gate.sh doctor
Run non-installing version/toolchain probes when you need reproducibility metadata:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-strict-verification-gate/run_lean_strict_verification_gate.sh doctor --probe
Scan a Lean file without running Lean:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-strict-verification-gate/run_lean_strict_verification_gate.sh scan \
--input formal/final/proof.lean \
--artifact-stage final_candidate
Optionally typecheck only when Lean is already installed:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-strict-verification-gate/run_lean_strict_verification_gate.sh verify \
--input formal/final/proof.lean \
--artifact-stage final_candidate \
--typecheck
For a user-managed Lake workspace, use the explicit Lake environment runner.
The helper requires a project root containing lakefile.lean or
lakefile.toml, records the project context, and still runs the scanner before
typechecking:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-strict-verification-gate/run_lean_strict_verification_gate.sh verify \
--input formal/final/proof.lean \
--artifact-stage final_candidate \
--typecheck \
--runner lake-env-lean \
--project-root /path/to/lean/project
Set AAS_LEAN or AAS_LAKE to select a specific already-installed local
executable. Invalid explicit paths fail closed instead of silently using a
different tool.
The helper never installs Lean, Lake, mathlib, npm packages, Python packages, credentials, services, or MCP servers. Missing Lean reports tool_unavailable.
Before any typecheck, the scanner blocks active:
#evalIO.Processrun_cmdunsafeinitialize@[extern]--allow-importFinal or claim-supporting artifacts also block on active sorry, admit, unsanctioned axiom, unknown trust base, or unreviewed generated proof text. Stubs may contain placeholders only when explicitly marked artifact_stage = stub.
When this skill is involved, consider these workflow templates (install via
the workflow-templates artifact profile, or --with-deps to pull backing skills):
informal-to-lean-formalization-runbook -- Local-first intake mapping an informal proof to Lean declarations with a scanner-first verification gate separating typecheck status from claim support.