用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt；运行前请先检查来源。
npx skills add https://github.com/hoanganhduc/ai-agents-skills --skill axiom-axle-mcp命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地？可下载 SkillsMP 当前能够提供的文件。
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.
正在显示 SKILL.md
| name | axiom-axle-mcp |
| description | Use when preparing optional AxiomMath AXLE MCP setup for manual formal-proof assistance. |
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/axiom-axle-mcp/run_axiom_axle_mcp.ps1" doctor
PowerShell runner target:
& "$runtime\run_skill.ps1" "skills/axiom-axle-mcp/run_axiom_axle_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 AXLE MCP setup. It never installs packages, starts an MCP server, writes MCP/client config, stores credentials, or calls AxiomMath services. It reports local readiness and emits manual configuration snippets with placeholders.
Check local readiness without running uvx:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh doctor
Emit a manual MCP config snippet:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh config-snippet
Run offline smoke:
bash "${AAS_RUNTIME_ROOT:-$HOME/.local/share/ai-agents-skills/runtime}/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh smoke
The emitted local stdio snippet uses command uvx and args ["--from", "axiom-axle-mcp==0.3.3", "axle-mcp-server"] with placeholder <AXLE_API_KEY>. The hosted URL https://mcp.axiommath.ai/mcp is manual setup only.
AXLE output is remote supplemental evidence. Record it as axle_remote_check, 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.