as an layperson's example[0], https://incredible.pm is WIMP, but the structured interaction interface of https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html is far easier to drive (and could've been keyboard driven) once one understands how to do so.

[0] although these are both trivial compared to a "real" prover, eg https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...

> I have even heard people claim that doing a machine proof should resemble playing a computer game

Those people should be laughed at

or at least given a lollipop?