Se ha añadido el ejercicio Demostraciones con Lean4 e Isabelle/HOL de que la unión del conjunto de los números naturales pares e impares es el conjunto de los naturales, propuesto originalmente el 31 de mayo de 2021.