Can autocomplete suggestions LSP be smarter?

Stream: lean4 dev

[Dan Abramov]

This is a slightly vague request but I'm wondering if there's any way to improve this situation:

Screenshot 2025-07-04 at 17.16.04.png

When you don't know the theorem you want to use, the LSP doesn't help in any way — i.e. it doesn't prioritize "matching" shapes. I wonder if it should?

This is particularly noticeable with AI — I'm trying to connect Claude Code to Lean LSP via https://github.com/oOo0oOo/lean-lsp-mcp, and it works, but the completions it gets are almost always irrelevant:

screenshot

If "matching goal" completions were prioritized (and same for rw), I think it could provide a productivity boost both to humans and to AI.

Has there been any existing thinking on this? Are there plans to improve autocomplete to be more "relevant" in any way? The question I think it should get better at answering is "what stuff that's locally available to me may help resolve the problem I have on the current line". I don't think the current tools are good at that.

[Dan Abramov]

Filed https://github.com/oOo0oOo/lean-lsp-mcp/issues/5 for a more concrete issue but the broader point stands

[Sebastian Ullrich]

Improvements are always possible but there are some very real limitations VS Code puts on completion regarding reasonable time budget and presentation. Thus tactics like apply? and rw? using the info view have a lot more freedom in this regard and AI systems should likely prefer them as well for their specific use cases.

[Marc Huisinga]

@Dan Abramov
The specific completions that you get in your screenshots are provided by VS Code itself when the language server doesn't provide any, not Lean. You can disable them using the 'Editor: Word Based Suggestions' setting.
I've mulled over disabling them by default a couple of times but I've heard from several users that they use these word-based suggestions when using auto-completion for completion, not discovery, so I've been holding off on it.

The specific issue for having the language server provide completions in this particular example is lean4#7696. It's a bit tricky, though.

what stuff that's locally available to me may help resolve the problem I have on the current line

One problem with this occurs even before the language server is involved: The expected type at some source location is quite unstable in a partial program. I've played around with prioritizing "matching" completions in the past, but it didn't feel consistent enough to be very useful.
Ultimately, I think that there would have to be some significant improvements to the error recovery in the elaborator before something like this becomes feasible. There's a couple of issues on GitHub already to track some ideas for improving it.