Left here deliberately so you can see what a rejection looks like. The claim is false and the kernel says so — and what it hands back is the goal it still had open, which is the part worth reading.

lean
import Mathlib
theorem sqrt_four_irrational : Irrational (Real.sqrt 4) := by
  norm_num
✗ the tool rejected this8413 ms
/work/Submission.lean:2:59: error: unsolved goals
⊢ False