25AI & Agent Tooling

25 entries

lean-lsp-mcpMCP server that gives agents diagnostics, goals, hovers and search through the Lean LSP.oOo0oOo/lean-lsp-mcp
lean4-skillsClaude Code skills and plugins for Lean work.cameronfreer/lean4-skills
Lean BeamExtends the Lean LSP server for agent- and tool-driven workflows.leanprover/lean-beam
LeanTool"Code interpreter" for Lean that LLMs can call.GasStationManager/LeanTool
AXLEAxiom's Lean engine for proof verification, manipulation and runtime tasks (MCP).
Archon HorizonWorkspace-first orchestration for long-running Codex or Claude Code sessions on Lean.frenzymath/Archon-Horizon
ArchonMulti-agent coding and proving workflows over a Lean project, driven by blueprint DAGs.frenzymath/Archon
Lean skillsOfficial agent skills for proofs, toolchain setup, bisection and more.leanprover/skills
LeanSlopCall LLMs from inside Lean code as black-box automation.kiranandcode/leanslop
AristotleHarmonic's formal reasoning agent, available via web, CLI and API.

REPLJSON REPL that reports errors, sorries and proof states.leanprover-community/repl
PantographMachine-to-machine interaction interface for Lean 4.leanprover/Pantograph
PyPantographPython interface to Pantograph.stanford-centaur/PyPantograph
leanclientDrive Lean from Python via the LSP.oOo0oOo/leanclient
Kimina Lean ServerFast, scalable server for checking Lean code in batches.project-numina/kimina-lean-server
LeanDojoExtract data from and interact with Lean repositories programmatically.lean-dojo/LeanDojo
LeanCopilotLLMs as copilots inside Lean.lean-dojo/LeanCopilot
llmleanLLM tactic suggestions from local or cloud models.cmu-l3/llmlean

LoogleSearch declarations by name, type pattern or constant (web).nomeata/loogle
LeanSearchClient#search syntax for LeanSearch, Loogle and LeanStateSearch from the editor.leanprover-community/LeanSearchClient
LeanExploreSemantic search engine with an MCP server.justincasher/lean-explore

VerinaBenchmark for verifiable code generation (code, specs and proofs).sunblaze-ucb/verina
CLEVERCurated Lean benchmark for verified code generation.trishullab/clever
VericodingTools and benchmarks for verified coding.Beneficial-AI-Foundation/vericoding
SorryDBContinuously updated benchmark built from sorrys in real projects.SorryDB/SorryDB