Various math examples using Lean 4