| name | axiom-axle-mcp |
| description | Use when preparing optional AxiomMath AXLE MCP setup for manual formal-proof assistance. |
Axiom AXLE MCP Setup
Windows Runtime Commands
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.
Runtime Helper
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.
Research Evidence Policy
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.
