Comment by cloudie78

It’s called LSP, any good editor supports it.

In fact, VSCode’s support for Lean is via LSP anyways.