# Axiom Axle MCP

> Use when preparing optional AxiomMath AXLE MCP setup for manual formal-proof assistance.

- Skill: `hoanganhduc/axiom-axle-mcp` (Agent Skill)
- Install (CLI): `npx skillmds@latest add hoanganhduc/axiom-axle-mcp`
- Raw SKILL.md: https://api.skillmd.com/api/skills/hoanganhduc/axiom-axle-mcp/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: hoanganhduc (https://skillmd.com/u/hoanganhduc)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/hoanganhduc/axiom-axle-mcp

---


# 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:

```powershell
$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:

```powershell
& "$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
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
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
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.