El objetivo principal de Calculemus es proponer ejercicios de demostración de resultados matemáticos usando sistemas de demostración interactiva, fundamentalmente Lean e Isabelle/HOL.
En los enunciados de los ejercicios se da la plantilla para Lean.
Las soluciones propuestas están en la versión 3.30.0 de Lean y en la versión 2021 de Isabelle/HOL. Las distintas soluciones están ordenadas desde las más detalladas a las más automáticas. Además, las soluciones están en este repositorio de GitHub.
Es recomendable, antes de leer las soluciones propuestas, intentar escribir demostraciones propias (en el caso de Lean se pueden probar en el navegador a través de este enlace).
En los comentarios se pueden publicar demostraciones distintas de las propuestas en Lean, Isabelle/HOL u otros sistemas (como Coq, Agda o PVS.