Notes on Lean

This website contains notes on the Lean language and proof assistant.

Using Lean with any LSP-compatible editor

Three challenges when using Lean with an arbitrary LSP-compatible editor are:

1. typing mathematical symbols,
2. proof interactivity that is not part of LSP (Language Server Protocol), and
3. interoperability issues between the official Lean LSP server and LSP-compatible editors in general.

The official Lean 4 VS Code extension and the lean.nvim plugin address these challenges by providing integrated editor-specific and Lean-specific enhancements that go beyond the capabilities of standard LSP.

For typing math symbols, there are many solutions that are not editor-specific.

For Lean-specific proof interactivity, a new option is Webleank, which connects any LSP-compatible editor to Lean editor sidekick applications.

Lspleank solves interoperability issues but does not, by itself, provide proof interactivity.