القائمة
Use when preparing optional LeanExplore MCP setup for Lean declaration search and formalization support.
يُحدَّد Prompt الذي يراجع المصدر أولًا بشكل افتراضي. يمكنك التبديل إلى أمر مباشر أو تنزيل نسخة محلية.
اقرأ SKILL.md وأي ملفات مرافقة يعرضها SkillsMP قبل أن تقرر التثبيت.
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
يتجاوز الأمر المباشر Prompt المخصّص للمراجعة. افحص المصدر قبل تشغيله.
npx skills add https://github.com/hoanganhduc/ai-agents-skills --skill lean-explore-mcpيبقى الأمر في سطر واحد. مرّر أفقيًا لمراجعته كاملًا قبل النسخ.
تفضّل نسخة محلية؟ نزّل الملفات المتاحة حاليًا لدى SkillsMP.
عرض SKILL.md
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.
Route VNU eOffice requests to an existing vnu_eoffice package or CLI: monitor updates, list latest incoming/outgoing documents, search by keyword, download attachments, and hand explicit file delivery to the authenticated host queue.
Use when the user wants to extract arXiv IDs or DOIs from research or RSS digests and turn them into getscipapers requests or manifests.
| name | lean-explore-mcp |
| description | Use when preparing optional LeanExplore MCP setup for Lean declaration search and formalization support. |
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.ps1" "skills/lean-explore-mcp/run_lean_explore_mcp.ps1" doctor
PowerShell runner target:
& "$runtime\run_skill.ps1" "skills/lean-explore-mcp/run_lean_explore_mcp.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 only for explicit optional LeanExplore MCP setup. It never installs packages, writes MCP/client config, stores credentials, downloads local data, or calls LeanExplore services during doctor, config, or smoke. On POSIX, its explicit serve command can start the reviewed in-process adapter for exactly lean-explore==1.2.1.
Check local readiness without running lean-explore:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh doctor
Emit a manual MCP config snippet:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh config-snippet --backend api
Use --backend local only after local data has been prepared outside this repo with LeanExplore's own tooling.
Run offline smoke:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh smoke
The emitted local stdio snippet uses the absolute managed run_lean_explore_mcp.sh wrapper with args ["serve", "--backend", "api"] or ["serve", "--backend", "local"]. Set AAS_LEANEXPLORE_SITE_PACKAGES to an absolute, owner-protected site-packages directory containing exactly lean-explore==1.2.1. API mode also uses the placeholder LEANEXPLORE_API_KEY; local mode assumes a user-managed LeanExplore cache such as ~/.lean_explore/cache/.
Never add --api-key or --api-key=<value> to the MCP command: process
arguments are observable outside the child. The managed POSIX wrapper captures
and removes LEANEXPLORE_API_KEY before helper/interpreter discovery and moves
it to a private inherited descriptor. The Python adapter consumes and closes
that descriptor before importing LeanExplore. It instantiates the 1.2.1 API
client and FastMCP app in-process; it never invokes the broken upstream CLI
bridge. Native Windows serve fails explicitly because private-descriptor
credential transport is not implemented there. Doctor, smoke, and placeholder
config generation remain available on Windows.
LeanExplore output is Lean declaration retrieval evidence. Record it as lean_declaration_search, never as formal_check. It cannot set local lean_check_status, satisfy placeholder or trust-base scans, replace statement-equivalence review, or promote formal support without local Lean/project evidence.
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.