A native desktop IDE for Lean 4 on macOS, Windows and Linux. Every proof re-checked by Tenet, an independent Lean 4 kernel. An MCP server for AI assistants, with Git and GitHub built in.
A desktop IDE for Lean 4, on macOS, Windows and Linux. Lean elaborates your proofs as you type. Tenet then re-checks each one it built. Created by Keith Adler, @keithadler on X.
Install · Compared with VS Code · New to Lean? · Features · AI assistants · How it works · Build from source · Shortcuts · Docs
Lean Studio is a native desktop app built only for Lean. It is not a plugin or a web view inside another editor. The tactic state gets a full panel. Every tactic in a proof is listed with what it changed. Each declaration you build gets a second, independent check from Tenet, a separate implementation of Lean's kernel.
Most people write Lean in VS Code with the official lean4 extension, and it's very good. Here's what Lean Studio has, side by side:
VS Code + lean4 Lean Studio ---:---::---: Goals and messages as you type, go to definition, hover, completion, rename, references ✓ ✓ Unicode input (\alpha), semantic highlighting, inlay hints, call hierarchy, trace trees ✓ ✓ Every step of a proof listed with what it changed ✓ Prove It: a portfolio of tactics tried on each sorry, with counterexamples when the goal is false ✓ Extract a goal as a lemma, with the hypotheses it needs ✓ Independent re-checking of every declaration by a second kernel (Tenet) ✓ Why a theorem isn't fully proved, and a map of what rests on sorry ✓ Per-declaration timing from Lean's profiler ✓ Search Mathlib in plain English, and Loogle, built in ✓ Proof walkthroughs as web pages; share links to the web editor ✓ A tutorial, goals read in English, errors explained, for people new to Lean ✓ C FFI: @[exte
From the project README.
Add the radar badge to your README — it shows your project was picked up by MCP Radar and links to this page:
[](https://mcp.liqiwa.com/s/keithadler--leanstudio.html)
Jacobian: an MCP server, CLI, and Python library that gives AI agents a composable toolbox of mathematical capabilities with inspectable artifacts and independent verification.
peopleworks/XAFLogicExplainerTeach your AI coding agent what your DevExpress XAF application actually does. Roslyn-based extraction of entities, controllers, business rules and Model Editor customizations.
omaekumiko2-create/kruLocal-first MCP password and credential manager for AI agents. Use passwords, API keys, SSH identities, and TOTP without exposing hidden plaintext to the model.
AndyShaman/telegram-business-bridgeConnect any AI agent to your personal Telegram via the official Business API — no userbot, no ban risk, no Premium. Agent reads & searches full history, drafts replies; every reply waits for your ✅. M
systempromptio/systemprompt-demoAI Governance Infrastructure — open gateway demo. Self-hosted systemprompt.io gateway in a single Rust binary: policy, audit trails, and cost attribution on every AI request, with the Systemprompt Bri
hojttaler/ResolvrFree, source-available desktop GraphQL client and IDE for macOS, Linux and Windows: tabs that survive crashes, collections in git-friendly files, environments that refresh tokens, flows as smoke tests
The top new MCP servers of the week, every Monday. No spam, unsubscribe anytime.