Related Servers

No user-submitted related servers found.

Related Servers

• Aristotle MCP Server

  septract

  A

  license

  -

  quality

  F

  maintenance

  An MCP server that wraps Aristotle's automated theorem prover for Lean 4, allowing AI assistants to fill in proofs, verify lemmas, and formalize natural language into Lean code.

  Updated 6 months ago (2026-03-05 18:47 UTC)

  13

  MIT

• axle-mcp

  Vilin97

  F

  license

  -

  quality

  D

  maintenance

  Integrates the AXLE (Axiom Lean Engine) CLI with AI assistants to provide comprehensive tools for Lean 4 proof engineering. It enables users to validate, repair, and transform Lean theorems through a remote API without requiring a local Lean installation.

  Updated 5 months ago (2026-03-06 09:23 UTC)

  2

• lean-mcp

  KrystianYCSilva

  A

  license

  -

  quality

  D

  maintenance

  Enables verification of Lean 4 mathematical proofs via MCP tools, allowing AI clients to compile and check theorems with Mathlib.

  Updated 6 months ago (2026-02-21 17:16 UTC)

  1

  MIT

• Formath MCP

  yutayamamoto

  -

  license

  B

  quality

  -

  maintenance

  Enables extraction of mathematical content from TeX papers and conversion to Lean code through a structured intermediate representation. Supports project scaffolding, entity management, and task tracking for mathematical formalization workflows.

  Updated a year ago (2025-08-15 00:08 UTC)

  14

• Lean LSP MCP

  oOo0oOo

  A

  license

  A

  quality

  A

  maintenance

  Enables LLM agents to interact with the Lean theorem prover through the Language Server Protocol, providing tools for analyzing Lean projects, accessing diagnostics, goal states, documentation, and searching for theorems using both local and external search services.

  Updated 21 days ago (2026-07-30 08:53 UTC)

  23

  475

  MIT

• leanscreen

  ibrahimmian36

  F

  license

  A

  quality

  B

  maintenance

  A calibrated faithfulness screen for informal↔Lean 4 statement pairs, served over MCP. It provides deterministic checks and deep LLM-based analysis to help draft Lean statements.

  Updated 7 days ago (2026-08-12 14:54 UTC)

  2

  6