lean4-claude-plugin

MCP Tool

Beneficial-AI-Foundation/lean4-claude-plugin

Lean 4 Claude Code Plugin: Native LSP + 17 MCP tools for theorem proving

Install

$ npx loaditout add Beneficial-AI-Foundation/lean4-claude-plugin

Platform-specific configuration:

.claude/settings.json

{
  "mcpServers": {
    "lean4-claude-plugin": {
      "command": "npx",
      "args": [
        "-y",
        "lean4-claude-plugin"
      ]
    }
  }
}

Add the config above to .claude/settings.json under the mcpServers key.

Reviews

Loading reviews...

Quality Signals

Quality Score2300

Stars

Installs

Last updated84 days ago

Security: B

New

Safety

Risk Levelmedium

Data Access

read

Network Accessnone

Details

Sourcegithub-crawl

Last commit12/31/2025

View on GitHub→

Embed Badge

[![Loaditout](https://loaditout.ai/api/badge/Beneficial-AI-Foundation/lean4-claude-plugin)](https://loaditout.ai/skills/Beneficial-AI-Foundation/lean4-claude-plugin)