lean-aristotle-mcp: Instructions file for Claude Code

CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

Code Quality Rules

NEVER ignore linting or type checking rules. If a check fails, fix the code properly. Do not:

• Add # noqa comments
• Add # type: ignore comments
• Add ignore rules to pyproject.toml
• Disable any checks in configuration

If a rule seems wrong for a specific case, fix the code structure to satisfy the rule properly.

Project Overview

This is an MCP (Model Context Protocol) server that wraps Harmonic's Aristotle theorem prover, enabling AI assistants to invoke automated theorem proving during Lean 4 development. The server exposes tools for proving theorems, filling in sorry statements, and formalizing natural language to Lean 4.

Build System

The project uses a Makefile that auto-detects the .venv virtual environment. Run make help for all targets.

Setup

make venv          # Create virtual environment
make install-dev   # Install with dev dependencies (ruff, mypy, pytest)

Code Quality

make check         # Run all checks (lint + type-check)
make lint          # Run ruff linter
make format        # Auto-fix lint issues
make type-check    # Run mypy

Testing

make test          # Run mock tests (default, no API key needed)
make test-api      # Run live API tests (requires ARISTOTLE_API_KEY)
make test-all      # Run all available tests
make test-lean     # Verify the test Lean project builds
make verify        # Full verification (lint + type-check + tests + lean)

Running

make run           # Start MCP server
make run-mock      # Start MCP server in mock mode

Build & Clean

make build         # Build wheel package
make clean         # Remove build artifacts
make clean-all     # Remove all generated files (build + test + lean artifacts)

CI

make ci            # Run CI locally with act (auto-starts colima)

Requires act and colima for local Docker.