Using Vim 9 with Lean
Warning
Using Vim 9 with Lean is significantly less well supported than with Neovim and the lean.nvim plugin.
To enable generic LSP (Language Server Protocol) functionality in Vim 9 when editing Lean files, you need to install some software.
You will also want to configure key mappings.
Non-LSP and non-editor functionality
The software documented in this guide does not provide editor UI features specific to Lean, such as those found in the Lean 4 VS Code extension. For interactive feedback on Lean code, you can use generic LSP features together with separate non-editor applications.