Prooftoys is a visual proof assistant and the engine behind Mathtoys (http://mathtoys.org). The Prooftoys implementation is based on Alonzo Church's simple type theory as formulated by Professor Peter Andrews under the name Q0. Simple type theory is suitable for construction of most of mathematics, comparable to first-order logic plus set theory. It uses a minimum of simple, understandable concepts, expressing them with a handful of axioms and inference rules.
This repo used to have the assets for the prooftoys.org website, but files related to the webiste are now at http://github.com/crisperdue/prooftoys-site/.