lean
import Mathlib

example : 1 + 1 = 2 := by
  norm_num
∎ verified by the kernel30100 ms