v2026.4.1

Oh hello there. Another new release of lean.nvim is out!
It's been 6 months since the last one, so this is a big one — the infoview has gotten a lot smarter, we've dropped two dependencies, and there are a bunch of quality-of-life improvements throughout.

What's Changed

Inline Images and SVGs in the Infoview

lean.nvim can now render images and SVGs directly in your terminal.
<img> tags with data URIs display inline as raster graphics, and SVG elements are rasterized via resvg — all using the Kitty graphics protocol.
This works in Kitty, WezTerm, Ghostty, and other terminals that support the protocol.

Images scroll and clip correctly within the infoview window, and are cached to avoid redundant decoding or rasterization on re-render.

SVG support requires installing resvg (brew install resvg or cargo install resvg).
Raster images work without any extra dependencies.
To disable terminal graphics entirely, set graphics = { enabled = false }.

Screen.Recording.2026-04-21.at.19.21.30.mov

Semantic Navigation in the Infoview

The infoview now supports structured navigation between goals, hypotheses, suggestions, links, and trace diagnostics.
Rather than scrolling or searching visually, you can jump directly to what you care about:

Key	What it does
<LocalLeader>g	move cursor to the first goal
]g / [g	next / previous goal
]h / [h	next / previous hypothesis
]s / [s	next / previous suggestion
]l / [l	next / previous link
]t / [t	next / previous trace diagnostic
<LocalLeader>s	accept (click) the first suggestion
<LocalLeader>S	move cursor to the first suggestion

navigation.mp4

Trace Search

You can now search through trace messages directly in the infoview (the client side of leanprover/lean4#10365).
Place your cursor on a trace diagnostic and hit <LocalLeader>/ to search — matching text is highlighted and matching traces are automatically uncollapsed.
An empty query restores the original.
After searching, n / N navigate between matches, and the last query is remembered.

trace-search.mp4

<Plug> Mappings for Everything

All lean.nvim mappings now have <Plug> names, making them properly remappable.
For example, to rebind the infoview toggle:

vim.keymap.set('n', '<leader>li', '<Plug>(LeanInfoviewToggle)', { buffer = true })

The full list of <Plug> names is in the README.

Dropped Dependencies: nvim-lspconfig and plenary.nvim

lean.nvim no longer depends on either nvim-lspconfig or plenary.nvim.
LSP attachment is now handled natively using Neovim's built-in vim.lsp APIs, and plenary's async has been replaced with a thin coroutine wrapper.
Your dependencies block can remove both.

If you were passing LSP configuration through lean.setup's config table, this is now deprecated — use vim.lsp.config('leanls', {}) instead.

Imports-Out-of-Date Detection

There are two situations where Lean can indicate that a file's dependencies are stale.
The more critical one occurs when a file is first opened and its imports need rebuilding — in this case the file cannot be checked at all until they are rebuilt.
The VSCode extension handles this by prompting you to restart the file, and lean.nvim now does the same: you'll see a prompt asking whether to restart, and confirming will rebuild the stale imports and re-check the file.

This behavior is customizable via the on_imports_out_of_date callback.
For example, to skip the prompt and always restart automatically:

require('lean').setup {
  on_imports_out_of_date = function(bufnr)
    require('lean.lsp').restart_file(bufnr)
  end,
}

Goal Diff Highlighting

When Lean marks a goal as inserted or removed (via diffInteractiveGoals), the goal prefix (⊢) is now highlighted with DiffAdd or DiffDelete respectively.
This matches the existing hypothesis-level diffing.

Diagnostic Signs in the Sign Column

When a diagnostic spans multiple lines, the sign column now shows guide characters marking the full range of the diagnostic rather than just its first line.
This makes it easier to see exactly which code a diagnostic covers, especially for errors in multi-line definitions or tactic blocks.

diagnostics.mp4

Infoview State Highlighting

The infoview window's background now changes when attention is needed — it uses leanInfoNCError when the LSP is dead and leanInfoNCWarn when the infoview is paused.
Both are customizable highlight groups.

Interactive Hover

Pressing K now opens an interactive hover popup where subexpressions are clickable — the same TUI system the infoview uses.
Click on a type to see its own type, press gd to jump to its definition, and so on.
The popup shows the full expression signature, the type rendered interactively, documentation, and import info.
When the RPC session is unavailable it falls back to the standard vim.lsp.buf.hover().

This can be disabled via lsp.enhanced_handlers.hover = false if it interferes with another plugin.

hover.mp4

Other Changes

• Additional pins now display in their own split windows rather than being concatenated in the main infoview buffer

  pins.mp4

• Infoview updates on cursor movement are now throttled — rapid scrolling (e.g. holding j/k) no longer floods the LSP with requests.
  Further performance improvements are coming

• Progress bar signs are now cleared when LSP clients stop, preventing stale signs from lingering

• Fractional width/height values are now supported for the infoview (e.g. width = 1/3), and are the new default

• Only syntax-highlight interpolation in s!"" strings, not all strings

• Correct the root directory when editing files in .lake/packages

• Better support for editing in the core lean4 repository itself (uses lean --server instead of lake serve when no lakefile is present)

• Support for Lean's RPC v1 format (leanprover/lean4#12905)

Contributors

Thanks to everyone who contributed to this release:

• @antinomie8 — syntax highlighting for ≠ and ^ as operators
• Benedict Christian Smit — lspconfig deprecation fix
• @lucianchauvin — fractional infoview dimensions
• @scott7z — diagnostic and configuration fixes
• @Vinh-CHUC — documentation fix

The wiki manual has also been updated to cover all of the above.

Until next time Neovim friends.

---

We recommend Neovim 0.12, which introduces vim.pack — a built-in package manager that makes external plugin managers optional.
There's nothing incompatible with 0.11 in this release, but if you're still on 0.11 you should pin to the nvim-0.11 tag.
Support for 0.11 will be dropped after a few months.

You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update or vim.pack on 0.12.

New Contributors

• @Vinh-CHUC made their first contribution in #448
• @scott7z made their first contribution in #486
• @antinomie8 made their first contribution in #495

Full Changelog: v2025.10.1...v2026.4.1