lean.nvim: Lean 4 support for Neovim, built around an infoview

A Lean 4 environment that lives in the editor you already use

lean.nvim is Neovim support for the Lean theorem prover, written in Lua and distributed under the MIT licence. The repository description is that short, and the project is more substantial than the description suggests.

The design assumption is that you are already a Neovim user and you want your Lean work in it, rather than in a separate Lean IDE with its own buffer management and its own key bindings. The README points to a manual on the project wiki for the full list of configuration options, key mappings and commands, which is a reasonable division of labour for a plugin of this size.

The version story is stated clearly. The README says lean.nvim supports the latest stable Neovim release, currently 0.12.x, as well as the latest nightly, and that if you are on an earlier version such as 0.10.x, your plugin manager can install the nvim-0.10 tag until you upgrade. The badge at the top of the README says Neovim 0.11 and later, which is the floor of what the plugin itself needs rather than the range it is tested against.

So the audience is people who write Lean 4 in Neovim, and the barrier to entry is not the plugin but the ecosystem it plugs into. The features read as a list of the things a Lean workflow needs: state feedback, commands, snippets, incremental information, and the interactive theorem provers rendered where you can see them.

The sponsorship note is also worth recording, because it explains the pace. A portion of the development is sponsored by the Lean FRO, and the README says plainly that the plugin would not be as featureful without that support.

Two installation paths, and a lazy trigger

On Neovim 0.12 or later, the install is two lines of Lua using the built-in package manager:

vim.pack.add { "https://github.com/Julian/lean.nvim" }

vim.g.lean_config = { mappings = true }

The second line is not configuration for the sake of it. The README points to the manual for what the mappings option does, and the obvious reading is that it is the switch for the key mappings, which is a common pattern in modern Neovim plugins that keep key bindings opt-in so they do not fight with your own.

For older Neovim, or if you do not want vim.pack, the plugin goes in through your plugin manager. The README's example uses lazy.nvim, and it shows the details that matter for a proof assistant plugin:

{
  'Julian/lean.nvim',
  event = { 'BufReadPre *.lean', 'BufNewFile *.lean' },

  dependencies = {
    -- optional dependencies:

    -- 'nvim-telescope/telescope.nvim', -- for Lean-specific pickers
    -- 'andymass/vim-matchup',          -- for enhanced % motion behavior
    -- 'andrewradev/switch.vim',        -- for switch support
    -- 'tomtom/tcomment_vim',           -- for commenting
  },

  ---@type lean.Config
  opts = { -- see the manual for full configuration options
    mappings = true,
  }
}

The event trigger is the interesting part. The plugin loads on BufReadPre and BufNewFile for .lean files rather than at startup, which is what you want from something that starts a language server and opens an infoview.

Every optional dependency is commented out, so nothing is pulled in by default. The four that are listed, telescope, vim-matchup, switch.vim and tcomment_vim, are integrations rather than requirements, and each one adds a capability rather than making the plugin work.

The infoview carries the proof state

The infoview is the centre of the plugin. The feature list describes it as showing persistent goal, term and tactic state, with interactive widget support for most widgets that can be rendered as text.

That is the part that changes how you work. A goal list, the terms in scope and the current tactic are the three pieces of state you would otherwise have to keep in your head or check in a separate window. Rendering them persistently means the proof state is visible while you edit the file that produced it.

The commands are the interface to all of that. The README lists user commands for interacting with infoviews, goals, diagnostics and the Lean server, and names three of them: :LeanGoal, :LeanInfoviewToggle and :LeanRestartFile. The restart command matters more than it looks, because the Lean server holds state per file and a restart is the escape hatch when that state and the buffer disagree.

Around the infoview there are smaller features that are the difference between a plugin and an environment. Abbreviation insertion for unicode characters works in insert mode and in the command window reached with q/. File progress information appears in the sign column for visible lines, so you can see at a glance which lines of a long proof are done. And if satellite.nvim is present, a satellite extension is registered to show the progress information for the whole document in its floating window.

The satellite integration is a good example of the plugin's approach in general. It does not implement its own status display, it detects a plugin that already does that job and registers an extension with it. The same pattern shows up with telescope, vim-matchup and switch.vim, each of which is treated as an optional peer rather than a dependency.

Optional peers: Loogle, matchup, switch and snippets

The integrations are worth listing individually, because each one plugs into something that already exists.

If telescope.nvim is present, a :Telescope loogle command becomes available as a frontend for the Loogle JSON API, which is the search backend for Lean's library. If vim-matchup is present, you get vim-matchup definitions for Lean, which improves the behaviour of the percent motion in a proof with many similar identifiers. If switch.vim is present, you get switch base definitions for Lean, so the switch tool knows how to jump between related declarations.

Snippets are handled in the VSCode compatible format, and the repository carries a package.json whose only content is a snippet contribution pointing at ./snippets/lean.json for the lean language. That file is meant to be consumed by something like vim-vsnip, which means a snippet library written for the Lean IDE ecosystem can be reused here rather than rewritten.

Semantic highlighting is supported, with the details in the manual and a sample colour scheme setup in the wiki. Semantic highlighting is the Lean 4 feature where the colouring of an identifier comes from the elaborator rather than from a syntax pattern, so a name that the elaborator has resolved to a particular type is coloured as that type. In an editor that does not understand it, everything falls back to plain syntax colours and the difference between two similar-looking names is lost.

One more integration is for scripts rather than people. The Lean library search path is available through lean.current_search_path(), which the README suggests is useful as a set of paths to grep or live grep within, and the wiki has a sample configuration for exactly that.

ProofWidgets drawn in the terminal, when the terminal can draw them

The optional graphics support is the feature that most depends on the environment around Neovim.

In terminals that support the Kitty graphics protocol, which is Kitty, WezTerm, Ghostty and others, lean.nvim can render images and SVGs from ProofWidgets inline in the infoview. So a goal that includes a diagram, a counterexample picture or a plot appears in place rather than as a placeholder.

The dependency requirement differs by format. SVG rendering requires resvg, which can be installed with brew install resvg or cargo install resvg. Raster images, which are img tags with data URIs, work without any extra dependencies at all. So a plugin user with a modern terminal gets some of the graphics for free, and the rest depends on whether they are willing to install a native renderer.

There is an escape hatch, and it is a single option: set graphics = { enabled = false } in your configuration to disable all terminal graphics.

That option is worth knowing about for a second reason. Inline images in a terminal are the kind of feature that can be a problem over SSH, in a terminal multiplexer with an unusual renderer, or on a system where the graphics protocol is half supported. Being able to turn it off in the configuration rather than by removing the plugin is the difference between a broken display and a slightly plainer one.

The test suite runs a headless Neovim with a clean config

The repository is unusually well organised for a Neovim plugin, and the justfile is the clearest evidence of that.

The test recipe is two steps. The test target rebuilds the test fixtures and clones the test dependencies, then calls retest, which runs the suite without doing either again. The retest recipe launches Neovim headless and clean with a minimal init file and asks the inanis test runner to execute the specs, with a per-test timeout of 180000 milliseconds, and with a sequential mode controlled by an environment variable.

The clean environment is the detail that matters. XDG_CONFIG_HOME is pointed at a separate .test-config directory, and the minimal init file lives in scripts/, so the suite cannot accidentally pick up your own configuration, your own plugins or your own key mappings. A plugin test suite that runs against the developer's real configuration passes for reasons that have nothing to do with the plugin.

There is a devcontainer recipe that builds and runs a LazyVim image using container on macOS and podman elsewhere, and a scratch recipe that opens a scratch buffer for interactive testing. The comment on that recipe is worth a mention, because it is the kind of note that saves someone an afternoon: still no idea why the extra :edit is required to get the LSP alive.

The repository also carries the linting setup you would expect, with a .luacheckrc for luacheck, selene.toml and selene-vim.toml for the selene linter, a .stylua.toml for formatting, a .luarc.json for the language server, a .pre-commit-config.yaml, a .markdownlint.jsonc for the documentation, and a justfile to tie them together. There is a .luacov file for coverage, a rockspec for a luarocks install, spec/ for the tests, demos/, doc/, lua/, plugin/, ftplugin/, indent/, syntax/ and snippets/ for the rest of the plugin.

Date-based versions, the Lean FRO, and a wiki as the manual

The release naming is calendar based: v2026.4.1 from 2026-04-22, v2025.10.1 from 2025-10-03, and v2024.12.2 from 2024-12-28. The year and month are in the version, so a user can tell from the tag alone how old their plugin is, and the ordering of versions is the ordering of releases rather than an arbitrary sequence.

The sponsorship arrangement is the other fact that shapes the project. A portion of the development is sponsored by the Lean FRO, and the README says the plugin would not be as featureful without that support. For an open source tool attached to a theorem prover, that is the arrangement you would hope for, since the people who benefit from better Lean tooling are the people who fund it.

Documentation is the weak point, and the README is candid about it. The full list of configuration options, key mappings and commands lives in a manual on the project wiki, with separate pages for syntax highlighting and for configuring and extending. A wiki is editable by anyone with an account, which makes it easy to improve and easy to break, and it is not versioned alongside the code. If you pin the plugin to a tag, you are relying on a wiki page that describes the current release.

The README closes with a list of other plugins it considers useful, and it is aimed at people who also use VSCode: nvim-lightbulb for signalling when code actions are available, goto-preview for peeking at a definition instead of jumping to it, and neominimap.nvim for people who like minimaps. The list is described as hopelessly incomplete, which is at least honest.

Overall, this is a focused, well tested plugin with an active maintainer, a real sponsor and a versioning scheme that tells you how old your copy is. Its costs are the wiki dependency and the fact that the interesting features, the infoview and the graphics, need your terminal to cooperate.

Editorial conclusion

lean.nvim suits Lean 4 users who already live in Neovim and want the proof state, the goal list and the tactic feedback in the same window as the source, without running the Lean IDE alongside their editor. It does not suit a beginner, because the plugin assumes familiarity with Lean tooling and sends configuration to a manual on a wiki, and it does not suit somebody on an old Neovim who cannot upgrade, since the fallback is a release tag rather than a maintained branch. Check three things before you adopt it: that your Neovim version is one it supports, that you understand the mappings option, since the key mappings are switched on separately from the plugin itself, and that the optional integrations you rely on, telescope, satellite or a terminal with graphics support, are actually present. The last push to the repository was on 2026-10-20 and the newest release is v2026.4.1 from 2026-04-22.

Frequently asked questions

Official sources

1. Issues
2. Julian/lean.nvim on GitHub
3. License: MIT
4. README
5. Releases