Lean4 LSP Configuration

The details below describe how to install and configure the Lean4 language server found here.

Installing the Language Server

A pre-built release of the language server can be downloaded from here.
In this case the lean-4.32.0-windows.zip release was used. Download the release zip file and complete the install by extracting the contents to a suitable installation folder, similar to the one shown below: 
 Directory of D:\Utilities\lean-4.32.0-windows

13/07/2026  09:04 PM    <DIR>          .
22/07/2026  01:56 PM    <DIR>          ..
13/07/2026  09:04 PM    <DIR>          bin
13/07/2026  09:04 PM    <DIR>          include
13/07/2026  09:04 PM    <DIR>          lib
13/07/2026  08:29 PM             9,231 LICENSE
13/07/2026  08:29 PM            83,431 LICENSES
13/07/2026  09:04 PM    <DIR>          share
13/07/2026  09:04 PM    <DIR>          src

The bin folder listed above will need to be added to the system PATH meaning the folder shown below needs to be added to that environment variable.

D:\Utilities\lean-4.32.0-windows\bin

Details on how to set the PATH can be found here.

With the software installed and the path updated, test the installation by running Lake.exe --version at the command line prompt, which should result in the following output: 
Lake version 5.0.0-src+8c9756b (Lean version 4.32.0)

Configuration

Start Zeus and use the Options, Document Types menu to edit the Lean4 document type and in the Language Server panel apply the following configuration settings: 
Program Type: Executable
     Program: Lake.exe
   Directory:
   Arguments: serve

Using the Language Server

To start using the language server create a test Lean project as follows:

md c:\Projects\LeanTest
cd c:\Projects\LeanTest
lake init

Use the Zeus, Workspace, Open Folder menu and open the c:\Projects\LeanTest folder as a Zeus workspace.

To test the configuration open the Main.lean file found in the workspace and fire off an autocomplete request as shown below:
lsp lean4
In addition to code completion, code navigation, function signatures and document hover should also work.
For example, the image below shows the result of a document hover over the println function.
lsp lean4 hover
IMPORTANT: If the autocomplete and hover do not fire, first wait a few moments as the Lake language server does take a little time to start. After that try closing then re-opening the Lean files.


Latest Version: Zeus 3.99e
Released: 16th July 2026
What's New