The Incredible Proof Machine es una herramienta visual e interactiva diseñada para realizar demostraciones en distintas lógicas —proposicional y de predicados, entre otras— mediante bloques que se conectan arrastrando y soltando. Cuando la conclusión aparece en color verde, el usuario ha completado una demostración válida. Su objetivo es transmitir la diversión de demostrar teoremas con ayuda del ordenador, sin necesidad de aprender antes la sintaxis de un demostrador formal tradicional como Isabelle.
La interfaz permite conectar dos puntos simplemente arrastrándolos; existen además bloques específicos, como el bloque ✎P para introducir fórmulas. Para las fórmulas se aceptan abreviaturas: "&" para la conjunción, "|" para la disyunción, "->" para el condicional, "^" para la NAND, "~" para la negación, "!" para el cuantificador universal, "?" para el existencial y "False" para la contradicción. Cada asunción y cada conclusión deben escribirse en líneas separadas.
La herramienta también permite seleccionar varios bloques manteniendo pulsada la tecla Shift y crear un bloque personalizado que los agrupe. Las demostraciones solo se guardan en el navegador local del usuario, por lo que se pierden al cerrar la pestaña o borrar el almacenamiento; los autores prevén habilitar guardado en servidor en versiones futuras.
El proyecto es software libre. Su autor principal es Joachim Breitner, con contribuciones de una comunidad de colaboradores. El código está disponible en GitHub (repositorio "nomeata/incredible") y se acompaña de varias publicaciones académicas, incluido un artículo presentado en ITP 2016 y un vídeo introductorio de 13 minutos en el canal Tea Leaves Programming. Está pensado tanto para uso educativo como para servir de base a nuevas contribuciones.