leanforge-mcp AGENTS.md

AGENTS.md -- leanforge-mcp

Agent protocols for Cursor, Windsurf, Claude Code, and any agentic IDE working in this repo.

Stack

• Language: Python 3.11+, FastMCP >= 3.2.0
• Package manager: uv
• Lean: Lean 4 via elan, Mathlib4
• Config: TOML via tomllib (stdlib, Python 3.11+)
• Persistence: SQLite via aiosqlite
• Linting: Ruff (formatter + linter)
• Tests: pytest + pytest-asyncio

Repo layout

leanforge-mcp\
├── src\
│   ├── core\
│   │   ├── agent.py        # Subagent loop: LLM propose → Lean compile → repeat
│   │   ├── config.py       # TOML config loader + dataclasses
│   │   ├── job_manager.py  # SQLite job queue, status tracking
│   │   ├── lean_client.py  # Lean 4 subprocess wrapper
│   │   └── llm_client.py   # Multi-tier LLM client (Ollama / OpenAI-compat / Anthropic)
│   ├── tools\
│   │   ├── submit.py       # submit_theorem, submit_lean_file
│   │   ├── status.py       # get_proof_status, list_attempts, list_jobs, validate_lean
│   │   ├── control.py      # cancel_job
│   │   └── mathlib.py      # get_mathlib_search
│   ├── lean\
│   │   └── templates\      # .lean file templates for common theorem shapes
│   └── server.py           # FastMCP server entry point + main()
├── tests\
│   └── test_pipeline.py    # End-to-end pipeline tests
├── docs\
│   ├── ARCHITECTURE.md
│   ├── LEAN_PRIMER.md
│   └── BENCHMARK_RESULTS.md
├── data\                   # SQLite DB lives here (gitignored)
├── logs\                   # Log files (gitignored)
├── workspace\              # Temp Lean files per job (gitignored)
├── config.example.toml
├── config.toml             # Local config (gitignored)
├── pyproject.toml
├── start.ps1
├── glama.json
├── llms.txt
├── AGENTS.md
├── CLAUDE.md
└── README.md

Critical rules

Lean subprocess

• lean_client.py shells out via asyncio.create_subprocess_exec -- never shell=True
• Lean path must come from config; never hardcode
• Capture both stdout and stderr; Lean emits errors to stderr
• Timeout every compile call (default 30s); Lean can hang on malformed input
• lean --stdin is faster than lake build for single-theorem proofs -- use it