Lean 4

Zed Lean 4

A Lean(4) Theorem Prover extension for Zed.

• Tree-sitter: tree-sitter-lean
• Language Server: Lean Language Server

Lean Toolchain

The Lean Language Server is integrated with the Lean toolchain. It is recommended to manage Lean toolchain versions via elan. For example, you can install the stable Lean version by running:

elan default stable
lean --version

Features

Highlight

• For optimal highlighting, set "semantic_tokens" to "combined", which will enable LSP semantic tokens highlight in Zed.

The extension provides automatic indentation, bracket matching and an outline for declarations, fields, constructors, aliases and anonymous instances. Bracket completion includes ⌈⌉, ⌊⌋, ⟦⟧ and ‹›. Word selection includes Lean identifier suffixes such as the ! in get! and the ? in find?.

In Vim mode, function and class text objects distinguish their bodies from the surrounding declarations. Each line comment is a separate comment object, so selections do not extend across blank lines. Namespace and section headers appear in the outline, but the grammar represents their contents as sibling commands and cannot provide enclosing namespace text objects.

Documentation comments support Markdown highlighting. The current grammar exposes each comment as one token, so the injected Markdown includes the Lean comment delimiters and covers only the Markdown-compatible part of Verso syntax. Put Markdown block constructs such as headings on a new line after /-- or /-!.

Indentation uses syntax ranges and a conservative line-based fallback for unfinished terms. The fallback skips lines containing double quotes or comment delimiters before the final layout keyword; it cannot distinguish arbitrary text inside multiline strings or block comments from code. The static grammar also approximates custom notation and some tactic/do syntax; LSP semantic tokens complement its highlighting.

Abbreviation

• Abbreviation (unicode character) insertion is supported by snippets.

Installation

• Firstly, the extension will check path and arguments in lsp.lean4-lsp.binary settings. Then it will search lake in $PATH, try $ELAN_HOME and default directory.
• If Lean 4 is not detected, this extension can automatically install elan with default toolchain. To enable this feature, you must set "elan_auto_install" to true. You can also specify the default toolchain by setting "elan_default_toolchain" to "stable", "nightly" or "v4.28.0".
• During installation, the extension will automatically add ~/.elan to your $PATH. The Lean toolchain can be completely removed by running elan self uninstall.
• If the Zed worktree is a parent directory of a Lean project, set lsp.lean4-lsp.settings.lean_project_dir to the project directory containing lakefile.toml (or lakefile.lean). Relative paths are resolved from the worktree root; absolute paths are also supported. This starts an automatically detected Lake with --dir so project dependencies such as Mathlib are available. A configured lsp.lean4-lsp.binary takes precedence; for that case, include "--dir", "/path/to/project" before "serve" in binary.arguments.

settings.json Sample

{
  "semantic_tokens": "combined",
  "lsp": {
    "lean4-lsp": {
      "binary": {
        "path": "/path/to/your/.elan/bin/lake",
        "arguments": ["serve", "--"]
      },
      "settings": {
        "elan_auto_install": true,
        "elan_default_toolchain": "stable"
      }
    }
  }
}

Nested Lean project

When the extension detects lake automatically, configure the Lean project directory relative to the Zed worktree root:

{
  "lsp": {
    "lean4-lsp": {
      "settings": {
        "lean_project_dir": "formalization"
      }
    }
  }
}

TODO list

• Implement infoview like VSCode and Neovim with Rust
• Tree-sitter-lean is experimental now and needs improvement
• Update and uninstall elan

Development

To develop this extension, see the Developing Extensions section of the Zed docs.