A few years ago, Edwin Zacharias published this beautiful “Tactical Proof System” (Sympathy for the Machine), written in Elm:
There also was an undocumented Hilbert Proof System application.
Unfortunately the original site has been down for a long time, and Edwin seems to be unreachable. It would be great not to lose this excellent work – it has been incredibly useful in teaching.
Would someone like to help me set it up again?
Or maybe knows Edwin so I can contact him?