Este blog es una continuación de Calculemus en el que se segurán proponiendo diariamente un ejercicio de demostración y publicando sus soluciones con Lean4 e Isabelle/HOL.