모형 Context 의정서 Axiom Lean Engine 용 서버 - Lean 노출 AI Agent에 검증 및 조작 도구.

설치

1. 무료 API 키 만들기: https://axle.axiommath.ai/app/console.
2. 당신의 클라이언트를 연결하십시오:

Claude (웹, 데스크탑, 모바일)

1. 오픈 사용자 정의 → 커넥터 → ** 추가 ** → ** 사용자 정의 커넥터 추가 **.
2. 이름: Axle. 원격 MCP 서버 URL: https://mcp.axiommath.ai/mcp.Add를 클릭합니다.
3. click Add 다시 기본 클라이언트 설정을 수락합니다.
4. ClickConnect를 클릭하고 로그인 페이지에서 API 키를 붙여넣기.
5. 채팅에서 ** + ** 메뉴 → ** 연결** 및 스위치 ** Axle**를 엽니다.

채팅GPT

유료 플랜 및 개발자 모드 필요 (Settings → Security and login).

1. ChatGPT 플러그인 열기 → ** + **.
2. 이름: Axle. MCP 서버 URL: https://mcp.axiommath.ai/mcp. 인증: OAuth.
3. 로그인 페이지에서 API 키를 만들고 붙여 넣으십시오.
4. 채팅에서 ** + ** → ** 개발자 모드 ** 메뉴에서 차축을 추가하십시오.

Claude 코드

그런 다음 /mcp 을 실행하고 열 페이지에 API 키를 붙여. 한국어 브라우저, 키를 직접 전달:

다른 MCP 클라이언트 (Cursor, Windsurf, VS Code, Cline, …)

AXLE MCP Server

A Model Context Protocol server for Axiom Lean Engine — exposes Lean verification and manipulation tools to AI agents.

Installation

1. Create a free API key: https://axle.axiommath.ai/app/console.
2. Connect your client:

Claude (web, desktop, mobile)

1. Open Customize → Connectors → Add → Add custom connector.
2. Name: Axle. Remote MCP server URL: https://mcp.axiommath.ai/mcp. Click Add.
3. Click Add again to accept the default client settings.
4. Click Connect and paste your API key on the sign-in page.
5. In a chat, open the + menu → Connectors and switch Axle on.

ChatGPT

Needs a paid plan and Developer mode (Settings → Security and login).

1. Open ChatGPT Plugins → +.
2. Name: Axle. MCP server URL: https://mcp.axiommath.ai/mcp. Authentication: OAuth.
3. Create it and paste your API key on the sign-in page.
4. In a chat, add Axle from the + → Developer mode menu.

Claude Code

claude mcp add --transport http axle https://mcp.axiommath.ai/mcp

Then run /mcp and paste your API key on the page that opens. To skip the browser, pass the key directly:

claude mcp add --transport http axle https://mcp.axiommath.ai/mcp \
  --header "Authorization: Bearer your_api_key_here"

Other MCP clients (Cursor, Windsurf, VS Code, Cline, …)

{
  "mcpServers": {
    "axle": {
      "type": "http",
      "url": "https://mcp.axiommath.ai/mcp",
      "headers": {
        "Authorization": "Bearer your_api_key_here"
      }
    }
  }
}

To run the server locally instead (enables file_uri, which reads Lean files from disk):

{
  "mcpServers": {
    "axle": {
      "command": "uvx",
      "args": ["--from", "axiom-axle-mcp", "axle-mcp-server"],
      "env": {
        "AXLE_API_KEY": "your_api_key_here"
      }
    }
  }
}

Tools

Most tools are generated from the AXLE API’s /v1/endpoints — verify_proof, check, merge, sorry2lemma and friends. Alongside them the server provides: