These integrations sit outside the core corpus workflow. Each path is suggest-only or operator-driven unless noted otherwise.
| Document | Purpose |
|---|---|
| mcp-lean-tooling.md | MCP server for listing Lean declarations |
| pandoc-latex-integration.md | Extract claims from LaTeX via Pandoc |
| prime-intellect-llm.md | LLM proposals for claims, mapping, and Lean (human-gated apply) |
Install extras as needed (uv sync --extra mcp for MCP tests). Each guide documents provider setup.