Se ha añadido el ejercicio Demostraciones con Lean4 e Isabelle/HOL de que los primos mayores que 2 son impares, propuesto originalmente el 1 de junio de 2021.