The Incredible Proof Machine (2016)

The Incredible Proof Machine was created to convey the fun and joy of doing proofs, especially in a computer aided way, without first having to learn the syntax of a “real” thereom prover like Isabelle. For more information about the Incredible Proof Machine, especially from an academic point of view, please see the following publications:

Most certainly! The more people contribute, the more incredible the The Incredible Proof Machine becomes.

Source: incredible.pm