Sympathy for the Machine: A lost tactical proof system

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?


There is an archived version of the original:*/

I tried out the archived version. It’s a pretty cool way to teach algebra.

I can’t help you set it up or contact Edwin but thanks for linking this!

you’re welcome! Let’s see if someone sees this who might be able to help out.

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.