Lean 4 — ZedExt

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.

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.lake_project_dir to the directory containing that project's lakefile.toml (or lakefile.lean). Relative paths are resolved from the worktree root. 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 Lake project

When the extension detects lake automatically, configure the nested project relative to the worktree root:

{
  "lsp": {
    "lean4-lsp": {
      "settings": {
        "lake_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.