[siraben]

I've been working on an interactive click-and-prove prover that is backed by dependently typed terms.[0] The Proof Machine only goes up to some Simply-Typed Lambda Calculus terms, whereas I have the logic sufficiently powerful to support recursion and reasoning about programs and equality.

[0] https://touchproof.siraben.dev/

[amavect]

I got stuck in a loop on 8 "Adding zero to the right", blindly following the tip below the box keeps looping induction introduction. Looping 9 times following the help tip, it eventually complains about an invalid proof state (kernel isn't general enough?). Where's the inductive hypothesis... doh the green box labeled IH on the left side. User error lol. But I feel that folks unfamiliar with proofs would struggle with it.

Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.

Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.

[siraben]

Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.

[amavect]

Just thought of how to fix the problem I had. Since the program already highlights the inductive hypothesis blue (but doesn't underline), consider adding a clickable underline to it (Rewrite with IH) instead of requiring the green IH box on the left (banner blindness). See if you can get rid of any drag&drop features and focus more on underline and click (TouchProof, not DragProof). Then the tip box would only need to explain clicking underlined terms.

And another thing, when 2 underlined terms nest (say, Sn+0=0 with underlines on Sn+0 and n), hovering should highlight only the more specific term (hovering on n highlights both Sn+0 and n the same color).