Lspleank
Lspleank is an LSP server that enables interoperability between:
- the official Lean LSP (Language Server Protocol) server (
lake serve) and - LSP-compatible editors without Lean-specific enhancements beyond standard LSP.
Editors with advanced Lean support
VS Code, Neovim, VSCodium, and Cursor, with their respective Lean-specific extensions/plugins, offer advanced, editor-specific support. For these editors, there is little reason to use Lspleank. You most likely want to follow the official Lean instructions.
Other editors
Programming in Lean
For programming in Lean, Lspleank might solve some of the issues you encounter when attempting to use your favorite LSP-compatible editor.
For reference information, including CLI help, see the lspleanklib repository
README.
Interactive theorem proving
By itself, Lspleank does not provide support for interactive theorem proving.
lspleank is a low-level CLI utility from the lspleanklib Python library.
It serves as an engineering stepping stone to Webleank,
which does provide Lean-specific features such as proof state interactivity.
As of early 2026, Webleank is in the very early stages of development and is not yet ready for general use.
Webleank interoperates with the lspleank utility and uses the lspleanklib Python package.