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

Recent Activity

got a basic "info panel" working. it shows the local assumptions and the current goal (at the cursor).
as in my previous demo, the first example shows using the rw tactic to use theorems to rewrite the goal into the form x = x, which is trivally true.
the second example shows unfolding definitions (negation is defined as P -> False) and introducing assumptions.
sadly, i only had two days to work on the project this week (so i didn't really get to the "interactivity" i had hoped for). still it was a lot of fun and i learned a couple of things 👌 &kibi-pa

got some basic proof tactics with manual proof goal inspection working. &kibi-pa