Geometry Prover

An MCP server that wraps AlphaGeometry2's DDAR (Deductive Database with Algebraic Reasoning) engine for geometry theorem proving.

Overview

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.

Tools

geometry_prove

Prove a geometry theorem using DDAR.

Input: Problem in AG2 format Output: Proof status and number of deduction steps

geometry_example

Get example problems from IMO competitions.

geometry_help

Documentation on the AG2 format and DDAR.

AG2 Problem Format

a@x_y = ; b@x_y = ; ...  (points with coordinates)
pred1, pred2, ...        (constraints)
? goal_predicate         (what to prove)

Predicates

• 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)

Architecture

┌─────────────────────┐
│   Mikey Agent       │
│   (Claude Code)     │
└──────────┬──────────┘
           │ MCP
           ▼
┌─────────────────────┐
│  mcp-geometry-prover│
│   (TypeScript)      │
└──────────┬──────────┘
           │ spawn Python
           ▼
┌─────────────────────┐
│  AlphaGeometry2     │
│  DDAR Engine        │
│   (Python)          │
└─────────────────────┘

Dependencies

• Node.js 18+
• Python 3.10+ with numpy
• AlphaGeometry2 repo at ~/Code/alphageometry2

Setup

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

Next Steps

1. Elvis Integration: Use local LLM to suggest auxiliary constructions when DDAR fails
2. Natural Language: Parse geometry problems from natural language
3. Proof Export: Generate human-readable proofs

License

MIT (wrapper code) Apache 2.0 (AlphaGeometry2)