i've been working on a programming language based on dependent type theory recently. it's primarily inspired by lean4.

one of the things i really liked about lean was its interactive proof assistant.

here's a screenshot of lean3 from the natural number game:

while you can see the proof state at each step (shown in the right panel), which is a lot better than seeing nothing at all (like in the left panel), there are many things that could be improved.

for one, the proof state panel only shows the proof state at the current cursor position. sometimes you need to move the cursor up and down through the proof to get an idea of what's going on.

the other major issue is indirect manipulation. sometimes, you want to apply a theorem, like a + b = b + a, to only some occurrences of the pattern a + b. it would be really convenient, if you could just click on the occurrences you want to replace in the proof state (instead of counting the occurrences and using nth_rewrite).

and ideally, i think it would be nice, if you could construct an entire proof just through direct manipulation in the proof state panel. but right now, i neither have a proof panel, nor proof tactics, so i'd better get to work :P