Zed Lean 4

A Lean(4) Theorem Prover extension for Zed.

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

Install Lean Toolchain

The Lean Language Server is integrated with Lean Toolchain. It's recommended to install nightly version via elan:

elan default nightly
lean --version

TODO list

• Tree-sitter-lean is experimental and needs improvement.
• Install, update and uninstall elan like VSCode
• Implement infoview like VSCode and Neovim.

Development

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