Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@mcp-geometry-prover a@0_0; b@1_0; c@0_1; ? coll a b c"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
An MCP server that wraps AlphaGeometry2's DDAR (Deductive Database with Algebraic Reasoning) engine for geometry theorem proving.
This server provides Mikey Agent with the ability to prove geometry theorems using the same symbolic reasoning engine that powered Google DeepMind's IMO gold-medalist performance.
Related MCP server: Aristotle MCP Server
geometry_proveProve a geometry theorem using DDAR.
Input: Problem in AG2 format Output: Proof status and number of deduction steps
geometry_exampleGet example problems from IMO competitions.
geometry_helpDocumentation on the AG2 format and DDAR.
a@x_y = ; b@x_y = ; ... (points with coordinates)
pred1, pred2, ... (constraints)
? goal_predicate (what to prove)coll a b c - collinear
cong a b c d - |AB| = |CD|
perp a b c d - AB ⟂ CD
para a b c d - AB ∥ CD
cyclic a b c d - concyclic
eqangle a b c d e f g h - ∠(AB,CD) = ∠(EF,GH)
┌─────────────────────┐
│ Mikey Agent │
│ (Claude Code) │
└──────────┬──────────┘
│ MCP
▼
┌─────────────────────┐
│ mcp-geometry-prover│
│ (TypeScript) │
└──────────┬──────────┘
│ spawn Python
▼
┌─────────────────────┐
│ AlphaGeometry2 │
│ DDAR Engine │
│ (Python) │
└─────────────────────┘Node.js 18+
Python 3.10+ with numpy
AlphaGeometry2 repo at ~/Code/alphageometry2
# Build
npm install
npm run build
# AG2 setup (one-time)
cd ~/Code/alphageometry2
python3 -m venv ag2_env
source ag2_env/bin/activate
pip install numpyElvis Integration: Use local LLM to suggest auxiliary constructions when DDAR fails
Natural Language: Parse geometry problems from natural language
Proof Export: Generate human-readable proofs
MIT (wrapper code) Apache 2.0 (AlphaGeometry2)
Get an example geometry problem in AG2 format
Inputs: problem_id (required).
Get help on the geometry prover and AG2 format
Inputs: no named parameters.
Prove a geometry theorem using AlphaGeometry2's DDAR engine.
Input format (AG2 problem string):
Points with coordinates: "a@x_y = ;"
Constraints: "coll a b c" (collinear), "cong a b c d" (congruent), "perp a b c d" (perpendicular), "para a b c d" (parallel), "cyclic a b c d" (concyclic), "eqangle a b c d e f g h" (equal angles)
Goal after "?": "cong e p e q" (prove EP = EQ)
Example (IMO 2000 P1): "a@-0.52_0.11 = ; b@-0.19_0.19 = ; ... cong a g1 g1 m, ... ? cong e p e q"
Returns proof status and number of deduction steps.
Inputs: problem (required).
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
Scored across 3 tools
Each tool has a clearly distinct purpose: one provides examples, one offers help, and one performs proofs. There is no overlap or ambiguity.
All tool names follow the consistent pattern 'geometry_<noun>', making them predictable and easy to distinguish.
With only three tools, the server is well-scoped for its specialized domain of geometry proving, covering essential functionalities without excess.
The tool set covers the complete workflow: getting started (example), learning (help), and executing proofs (prove). No obvious gaps are present.
Certified program synthesis. Pay per call in USDC via x402; refusals never billed.
Newton MCP — wraps the Newton math solver API (free, no auth)
Exact arithmetic, algebra, calculus, physics, chemistry and finance with a checkable formula.
Deterministic reasoning stack for AI agents: simulate, decide & compute, plus cross-domain tools.
