Learning Lean 4 and trying to prove something using it is extremely mentally stimulating.