Writing proofs by clicking

Abstract: In this talk I will present a prototype system that allows you to construct a Lean proof without typing any tactics or lemmas, by simply clicking in the infoview. This builds upon my work on the `rw??` tactic that is in mathlib. This kind of tool is very useful for writing proofs, especially to beginners, and it would also make a great addition to the natural number game.

You can try `#infoview_search` yourself. It can be found at github.com/JovanGerb/infoview_search

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026