lean
import Mathlib

example : 1 + 1 = 3 := by
  norm_num
✗ the tool rejected this18913 ms
/work/Submission.lean:3:23: error: unsolved goals
⊢ False