Jovan Gerbscheid - Writing proofs by clicking

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic for the talk.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

For enabling infoview_search everywhere, does calling addPanelWidgetGlobal instead of addPanelWidgetLocal not work? Are the refs above causing issues for importing?

[Snir Broshi]

For posterity, I asked: you added a ranking to find the best match for a selection, would it be possible to also find near-misses and show why they don't match? Sometimes a rw using a local hypothesis seems possible but there's a type mismatch that's impossible to see.
The answer was that the current data structure (discrimination tree) can't find near-misses, but it can find instance mismatches, which can help when there are diamond problems.
(this is the context for the question if anyone is interested #lean4 > Error messages suggestions @ 💬)

[Snir Broshi]

btw this is how I looked during the talk: :star_struck:

[Jovan Gerbscheid]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

For enabling infoview_search everywhere, does calling addPanelWidgetGlobal instead of addPanelWidgetLocal not work?

I think this should work, indeed. There are 2 small concerns:

• If this were to be imported in mathlib in the future, I think it might be polite to not turn it on in projects that depend on mathlib. What we could do is to have a set_option that is false by default, set to true in mathlib (in the lakefile), and the widget doesn't show anything if if the option is set to false.
• There is a startup cost of 5-10 seconds when writing #infoview_suggest. The advantage of having the #infoview_suggest command is that you don't need to wait for this the first time that you shift-click. This is not a big problem, thanks to the RefreshComponent because it can let you know that it is still starting up.

[Jovan Gerbscheid]

Snir Broshi said:

(this is the context for the question if anyone is interested #lean4 > Error messages suggestions @ 💬)

Since the mismatch is in the types, the lemma in question will indeed not be found unfortunately.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Jovan Gerbscheid said:

• If this were to be imported in mathlib in the future, I think it might be polite to not turn it on in projects that depend on mathlib.

That makes sense. One could also have a dedicated module Mathlib.Tactic.Widget.InfoviewSearch (or whatever name) importing which enables the widget globally, but which would be linted to prevent importing it outside of development; but an option sounds more ergonomic.

[Jovan Gerbscheid]

There is a small problem when using #infoview_search to add a rewrite into an existing chain of rewrites, namely that the tactic state doesn't update. It does update after you move the cursor (which is what I did during the talk).

The problem is that the cursor position didn't change, so the tactic state doesn't have a reason to update. Does anyone have an idea how to fix this?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hm, the tactic state should update when the file is reelaborated, even if the cursor hasn't moved. If it doesn't, there might be unsound caching happening somewhere.

[Jovan Gerbscheid]

It's a bit hard to reproduce this without the widget, because whenever I edit something in a file my cursor also moves...