Lean Studio MCP server

A Lean proof is only as trustworthy as the kernel that accepted it. Lean Studio doesn't take one kernel's word for it. Every declaration you build is re-checked from the compiled .olean files by Tenet, a separate implementation of Lean's type checker. If Lean's kernel had a bug, Tenet would have to repeat the same bug to agree. Each theorem then shows, in the gutter, whether it is really proved, rests on sorry, or rests on an axiom, and Why? takes you to the lemma responsible.

Around that sits a complete IDE built only for Lean. It is a native app, not a plugin or a web view inside another editor. The tactic state gets a full panel, every step of a proof is listed with what it changed, Prove It tries 17 tactics on any sorry at once, and a tutorial, plain-English goals and explained errors make it the place to start if you are new to Lean.

brew install --cask keithadler/tap/lean-studio    # macOS

Windows and Linux: download from Releases, or see Install for winget and the AppImage. It is free and open source.

Tested on a real result: ζ(5) is irrational

In September 2026 Lean Studio ran @mo271's formalization that ζ(5) is irrational (mo271/zeta5), about 218,000 lines on top of Mathlib, start to finish on a Mac:

Step	Result
Mathlib cache	8,700 files in 2 minutes
Build, 8,951 jobs	No errors, in about 43 minutes
Solution.lean	No errors and no sorry
Tenet's independent re-check	14,953 declarations in 213 modules, in 8 minutes: 14,952 verified, 0 rejected. The one resting on sorry is the challenge statement, as intended.
Axioms under irrational_five	propext, Classical.choice and Quot.sound, and nothing else

The statement Solution.lean proves is exactly the one in Challenge.lean, which is copied verbatim from Google DeepMind's Formal Conjectures. Any Lake project gets the same treatment: open it, Build, and Verify with Tenet.

How it compares

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		✓
A profiler: live as you edit, flame graphs, cost per tactic line, heartbeats, simp and instance counters, and a heartbeat regression check for CI		✓
Search Mathlib in plain English, and Loogle, built in		✓
Sorry Burndown: the project's sorry count over its last commits, from Git, and a branch's added, removed and restated theorems with proofs ignored, as Markdown for the pull request		✓
Junk values: where Lean quietly returns a made-up value (sInf of an empty set, xs[i]!, x / 0), so a definition or statement can compile while describing something that does not exist		✓
Docstring claims: a definition said to be equivalent to another with no theorem stating it, or a docstring that claims generality the definition's hypotheses lack, the prose that lets a wrong definition pass a cursory read		✓
Definitions that changed under unchanged theorems: the statement diff lists each definition whose body changed, whether its docstring changed with it, and the theorems that mention it		✓
Mathlib housekeeping: sort imports, tidy whitespace, wrap long comments, add the copyright header, delete old deprecations, a Mathlib-style name for a theorem, theorems that state the same thing, a project health summary		✓
Proof walkthroughs as web pages; share links to the web editor		✓
An onramp for people new to Lean: a tutorial, a puzzle a day with hints, goals read in English, errors explained, a hint for the goal under the cursor, a warning when a tutorial is Lean 3, practice typing symbols, badges for your firsts		✓
Projects the size of Fermat's Last Theorem: which sorry to prove next, which block the most, work split fairly among N people, how old each is, a completion forecast, the build's critical path, locked theorem statements, module layer rules		✓
C FFI: @[extern] checked against the C code, stubs, clangd		✓
Built-in AI that prefers a model on your computer (Apple's on-device model on macOS 27, Ollama, LM Studio, llama.cpp, MLX), with every proof it suggests checked by Lean before you see it		✓
An MCP server so AI assistants can use Lean		✓
ProofWidgets and other JavaScript widgets in the infoview	✓	✓ (Lean's own infoview, in the window or a browser)
Vim mode	✓ (an extension)	✓ built in
Integrated terminal, side-by-side diffs, merge-conflict actions, sticky scroll, breadcrumbs, minimap, Markdown preview	✓	✓
AI completion as you type	✓ (Copilot, an extension)	✓ checked by Lean before it is shown
Lean on another machine, in a dev container or in WSL	✓ (no mount needed)	✓ (SSH needs the folder mounted)
The VS Code ecosystem: its other extensions, Codespaces, the browser, Live Share	✓

Lean Studio is tested against real Lean on macOS, Windows and Linux on every change, and against a real Mathlib project every week.

New to Lean?

Lean Studio is built to be the place to start, whether you're curious about theorems or you write code. Everything below is inside the editor, in the Learn menu (and the command palette), with nothing to install but Lean Studio itself.

The onramp

1. Start playing. Open the Playground: one Lean file to experiment in, with no project to set up. #eval and #check answer at the end of their own line, like a notebook, and a file with a main gets a ▶ Run button. Pick a snippet (a function, a structure, a pattern match, a proof by induction, a calc chain) and fill it in.

2. Learn in order. The tutorial is ten short lessons, in Lean files, from #eval 2 + 2 to induction and proving your own programs correct. Each ends in exercises (sorrys to replace), and the Learn tab ticks a lesson off when Lean accepts it. Every exercise is checked against real Lean by the tests, so none is impossible. Famous theorems (addition is commutative, reversing a list twice, the law of excluded middle and, with Mathlib, infinitely many primes and √2 is irrational) come with a plain-English statement, and "Try it in Lean" shows the exact statement and the axioms it rests on.

3. Practise, with a puzzle a day. New Puzzle opens a small proof to finish: twelve of them, easiest first, from 2 + 2 = 4 to "there is a number whose square is 49". Replace the sorry and Lean tells you at once. Puzzle Hint gives a bigger hint each time you ask, and Show Puzzle Solution is there when you have really tried. Today's puzzle comes first. Every solution is checked against real Lean by the tests.

4. Get unstuck without being told the answer.

• Hint for This Goal reads the goal under your cursor and gives three hints, each a little bigger: what it says in words, what kind of goal it is ("an if-then: assume the left side"), and the tactic to try, written out.
• Explain This Declaration in Plain English reads a def, theorem, structure or inductive aloud: "double is a function. Given n (a natural number), it gives back a natural number."
• Hover any tactic or keyword (intro, simp, omega, theorem) for what it does, in plain words, with an example. The Proof Steps list explains each step's tactic too.
• Goals in words, under each goal: "In words: For all propositions p and q: if p and q, then q and p."
• Errors in plain words. Under Lean's message, "What this means" gives the gist of "unsolved goals", "type mismatch", "unknown identifier" and more than twenty others, and what to try.
• My Cheat Sheet collects the tactics and keywords your file actually uses, each explained with an example, in the order you first used them. You learn from what you have already written.

5. Dodge the traps.

• Is This Lean 3? Most tutorials, forum answers and blog posts online are about Lean 3, which looks like Lean 4 and does not run in it. Paste something in and this finds begin … end, λ x,, assume, cases h with x hx, lower-case imports and more, and says what each is now.
• Surprises in This File explains the things that catch people who already program: 3 - 5 is 0 for natural numbers, 7 / 2 is 3, 7 / 0 is 0, decimals are approximate, == is not =, and a natural number never overflows. None of them is a mistake: they are how Lean works, and each says why.

6. Type the symbols. Practice Typing Symbols opens a worksheet in the editor: each line names a symbol (for all, there exists, an arrow…) and shows what to type (\forall and a space). Type it where the real abbreviation input works, then Check My Symbol Practice marks each line. The symbol palette in the Learn tab inserts ∀ ∃ → ℕ ⟨⟩ and the rest with a click and shows how to type each, and hovering any symbol in your code does the same.

7. Coming from another language? Coming From… writes out how a Python, Haskell, JavaScript or Rust idea is said in Lean: a function, if/else, a list, map and filter, a record, printing, "maybe nothing", a loop, a comment.

8. See how far you have come. My Badges and What's Next scores small firsts, worked out from the Lean files you have written (so there is nothing to track): your first #eval, first function, first proof Lean accepts with no sorry, first induction, and so on, seventeen in the order you meet them, and it tells you what to try next. Tip of the Day shows one small thing that makes Lean nicer.

9. Start a real verified project. New Project… offers three templates of Lean Studio's own, each a small program that is already fully proved, laid out the way verified code stays honest: Spec.lean (what it should do, written to be obviously right), Impl.lean (what runs), Proofs.lean (why they agree, for every input), Tests.lean (known answers), a README explaining the layout, and the assurance check in CI.

• Verified crypto primitive: modular exponentiation by square-and-multiply, the operation underneath RSA and Diffie–Hellman, proved equal to b ^ e % m, with Diffie–Hellman agreement proved and the textbook RSA example as a test.
• Verified parser: prefix arithmetic expressions, with the round trip parse (print e) = some e proved.
• Verified file format: tag-length-value records, the shape of TLS and ASN.1, with decoding an encoded file proved to give back exactly its records.

Each starts at 100% on the assurance report: no sorry, no axiom, no native_decide, and a theorem about every definition.

The Outline also shows, live, which theorems Lean accepts (✓), which still use sorry (◐) and which have errors (✗).

Very large projects

Fermat's Last Theorem and Navier–Stokes are not one file; they are hundreds of files and thousands of declarations, with a team and a blueprint. The Big Projects menu (and the command palette, and the MCP server) reads the whole project as one dependency graph, with no Lean running, and answers the questions a project lead asks. On 36,000 declarations in 600 files it takes about a second.

1. Sorries to Prove Next: the sorrys you can prove right now, because everything their statements use is already proved, biggest unblocker first.
2. Sorries Blocking the Most: the sorrys that most other declarations rest on, directly or not.
3. Share Out the Work for N People: the open sorrys in N balanced packages, each kept together by file so people do not collide.
4. Oldest Sorries: how long each sorry has stood, by git blame.
5. Completion Forecast: the burndown continued, with the date the last sorry would go at the recent rate.
6. Build Critical Path: the import chain that sets the minimum build time however many cores you have.
7. Longest Proofs: the proofs most worth splitting.
8. Where to Split This File: groups of declarations that share nothing, so a long file can be cut cleanly.
9. Module Layers: list your layers, lowest first, in .leanstudio/layers.json ({"layers": [["Foundations"], ["Algebra"], ["Geometry"]]}) and the editor finds the imports that point upward.
10. Lock Statements: freeze every theorem statement (not proof) as a hash, and later see which statements changed. A blueprint formalized by many hands stays faithful.

Features

Five things other Lean editors don't do

1. ⚡ Prove It. Put the cursor on a sorry and press ⌘⌥P (Ctrl+Alt+P), or click ⚡ Prove it in the Tactic State. Lean Studio tries rfl, decide, simp, omega, norm_num, ring, linarith, nlinarith, positivity, aesop, grind, exact? and more on that goal. Each tactic runs separately from the same state, with its own time budget, in a single pass of Lean. You see every one that closes the goal and how long it took; one click puts it in place of the sorry. Every sorry in the file does the whole file at once, and Fill in every sorry it proved applies them all. A search tactic like exact? is replaced by what it found (exact Nat.mul_comm a b), so the proof doesn't search again on every check. Tactics that your imports don't provide (Mathlib's, in a file without Mathlib) are skipped rather than breaking anything.

   

2. Why isn't this proved? When Tenet says a theorem rests on sorry or on an axiom, Why? (in the Tenet panel, from the ◐ badge in the gutter, or from Tenet ▸ Why Isn't This Proved?) shows the chain of lemmas from that theorem down to the sorry. It finds the shortest chain through what each declaration uses, and marks the lemma that uses the sorry itself. Every link opens its source. In a big project, it answers "which lemma, three files away, is still unfinished?" in one click.

   

3. A profiler. Lean ▸ Profiler ▸ Profile File (⌘⌥T, Ctrl+Alt+T) runs Lean's own profilers over the file and opens the Profiler panel. Every declaration is listed by how long it takes to check, costliest first, with the step inside it that costs the most (omega, a simp call, an instance search, the kernel). Click one for its details, and pick what to see beside it:

   • a flame graph of Lean's trace, every step as wide as its cost and the steps inside it underneath, coloured by the kind of work; click a step to zoom in on it;
   • bottom up: every step summed by what it is, so twenty cheap simp calls add up in one row;
   • tactic lines: the cost of each line of the proof, which the editor also shows at the end of the line;
   • Lean's profiler: Lean's time per category (elaboration, type class inference, simp, type checking, compilation) and per tactic;
   • counters: what it made Lean do, from set_option diagnostics true: the simp lemmas it tried and how many of those worked, the instances it used, the definitions it unfolded.

   This declaration profiles only the one at the cursor, so it is quick to repeat while you tune a proof. Heartbeats measures Lean's heartbeats instead of time: the unit of maxHeartbeats, the same on every run, with each declaration's share of the limit. Times vary a little between runs, so Median of 3 or 5 runs Lean again and shows how much each time varied. Live profiles as you edit: a copy of the file with Lean's profilers on stays open in the running Lean server, and a moment after each change the panel and the editor show every declaration's cost as it is now, with the full trace of the one you are editing (any other's is fetched when you pick it). Lean re-checks only from your edit down, so this costs about what the edit does: on a 1,300-line Mathlib file, an edit shows in two seconds. Baseline sets what to compare with: this profile, the file as last committed, any branch or commit (profiled with today's toolchain and imports, so only the file's own change counts), or a profile saved earlier (every profile is kept, with the commit it was taken at). Each declaration then shows its change, live too. Under More, Check for Regressions runs the same check as CI (below), Profile Whole Project profiles every file and lists the costliest declarations of all of them, Copy as Markdown gives a table for an issue or Zulip, and Save for the Firefox Profiler saves Lean's trace for profiler.firefox.com. The last build's slowest modules are under Build. It profiles unsaved text, and your file is never modified.

   

4. Proof walkthroughs and share links. File ▸ Export Proof Walkthrough… writes every tactic proof in the file to one self-contained web page, step by step. Each step shows the tactic, what it does in plain words, and the goals before and after, exactly as Lean reported them. You can step through with ← and →. It works for a class handout, a blog post or a code review, and readers don't need Lean installed. Open in the Lean 4 Web Editor and Copy Share Link give a link that runs the file at live.lean-lang.org, which has Mathlib.

5. Ask Mathlib in plain English. The Library panel takes a description, such as "the sum of the first n odd numbers is n squared" or "a continuous function on a closed interval attains its maximum". It returns the Mathlib results that say that, with their informal statements, using LeanSearch. Loogle (below it) finds what you can name or write the shape of. This finds what you can only describe.

AI assistants get all five too: the prove, why_not_proved, profile, export_walkthrough and search_mathlib tools.