Moonshot Math

by tonicco.huggingface.tonic/math

Formal reasoning model that can reason and prove theorems

  • Remote endpoint
  • 1 tool
  • MIT

Uptime

Checked  · every day

100%from 4 days of checks

Up without downtime on 4 of 4 days with data.

  • No downtime
  • Degraded
  • Down over 5 minutes
  • No data
  • Not checked yet

Response time

Median 1198 ms, slowest 5% 1441 ms for the handshake and the tool list, over 30 days.

1500 ms750 ms0

How far each check got

  • Reached the address 100%
  • Completed the handshake 100%
  • Listed its tools 100%

1 tool at the last answer.

Every day
DayResultChecksMedian
3 Nov (today)No downtime11297 ms
2 NovNo downtime1of 11156 ms
1 NovNo downtime1of 1967 ms
31 OctNo downtime21204 ms

A failure counts as down time only when a second check five minutes later fails too. How we check

Connect to the publisher's own endpoint

Add to .vscode/mcp.json:

{
  "servers": {
    "math": {
      "type": "sse",
      "url": "https://tonic-math.hf.space/gradio_api/mcp/sse"
    }
  }
}
For agents: the install prompt

Every step above as one Markdown text, for an assistant installing it for you.

# Install the MCP server Moonshot Math (`co.huggingface.tonic/math`)

Its page: https://plug.directory/servers/co.huggingface.tonic/math

It runs on the publisher's servers; the client connects to its URL.

Use the section for the person's client.

## Claude Desktop

Paste into Settings › Connectors › Add custom connector:

```text
https://tonic-math.hf.space/gradio_api/mcp/sse
```

## Claude Code

Run in a terminal:

```sh
claude mcp add --transport sse math https://tonic-math.hf.space/gradio_api/mcp/sse
```

## Cursor, Devin Desktop, LM Studio, Gemini CLI, oterm, ECA

Merge into the place for the person's client:

- Cursor: ~/.cursor/mcp.json
- Devin Desktop: ~/.config/devin/mcp_config.json
- LM Studio: mcp.json (Program › Install › Edit mcp.json)
- Gemini CLI: ~/.gemini/settings.json
- oterm: config.json in oterm's data folder (~/Library/Application Support/oterm on macOS, ~/.local/share/oterm on Linux, %APPDATA%\oterm on Windows)
- ECA: ~/.config/eca/config.json (global) or .eca/config.json in the project

```json
{
  "mcpServers": {
    "math": {
      "url": "https://tonic-math.hf.space/gradio_api/mcp/sse"
    }
  }
}
```

## VS Code

Merge into .vscode/mcp.json:

```json
{
  "servers": {
    "math": {
      "type": "sse",
      "url": "https://tonic-math.hf.space/gradio_api/mcp/sse"
    }
  }
}
```

## Zed

This server's endpoint speaks only SSE, which this client's documentation does not list among its transports; use another client for it.

## Cline, AnythingLLM, Augment Code

Merge into the place for the person's client:

- Cline: cline_mcp_settings.json (MCP Servers › Configure › Configure MCP Servers)
- AnythingLLM: anythingllm_mcp_servers.json in the AnythingLLM storage plugins directory
- Augment Code: Augment Settings Panel – MCP section – Import from JSON (VS Code extension)

```json
{
  "mcpServers": {
    "math": {
      "type": "sse",
      "url": "https://tonic-math.hf.space/gradio_api/mcp/sse"
    }
  }
}
```

## Continue

Merge into ~/.continue/config.yaml:

```yaml
mcpServers:
  - name: "math"
    type: sse
    url: "https://tonic-math.hf.space/gradio_api/mcp/sse"
```

## Goose

This server's endpoint speaks only SSE, which this client's documentation does not list among its transports; use another client for it.

## Codex

This server's endpoint speaks only SSE, which this client's documentation does not list among its transports; use another client for it.

## mcp-client-cli, TUUI, BoltAI, Bob Shell, Kiro, Kiro CLI

This server's endpoint speaks only SSE, which this client's documentation does not list among its transports; use another client for it.

## Agenvoy

This server's endpoint speaks only SSE, which this client's documentation does not list among its transports; use another client for it.

## Amp

Merge into ~/.config/amp/settings.json (user) or .amp/settings.json (workspace):

```json
{
  "amp.mcpServers": {
    "math": {
      "url": "https://tonic-math.hf.space/gradio_api/mcp/sse"
    }
  }
}
```

Then restart the client, or reload its MCP servers, and ask it to list the server's tools to confirm it started.

Tools 1

  • Math_chat_handler Handles a single chat interaction with the Kimina Prover model designed for competition-style problem solving it is capable of both formal and informal mathematical reasoning and problem solving. Returns: (, List of (role, content) pairs for display in the chat UI., JSON string containing model input, output, extracted Lean4 code, and updated chat history., Extracted Lean4 code from the model's response, if present., Updated chat history including the latest user and assistant messages., ), , , UU, UU, UU, (X → P) → P, (Y → P) → P, X × Y → P, X, ============================, (Y → P)", >>> informal_prefix = "/-Explain using mathematics-/, ", >>> max_tokens = 1234, >>> chat_history = None, >>> display_history, output_data_json, code, chat_history = chat_handler(user_message, informal_prefix, max_tokens, chat_history), # display_history contains the chat turns, output_data_json contains the full model output, code contains extracted Lean4 code.

From Hugging Face Spaces. Report a problem