Se ha añadido el ejercicio Demostraciones con Lean4 e Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)", propuesto originalmente el 28 de mayo de 2021.