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

```bash
# 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)