Wrong proof test: 1 + 1 = 3
import Mathlib
example : 1 + 1 = 3 := by
norm_num
✗ the tool rejected this18913 ms
/work/Submission.lean:3:23: error: unsolved goals ⊢ False
import Mathlib
example : 1 + 1 = 3 := by
norm_num
/work/Submission.lean:3:23: error: unsolved goals ⊢ False
Sign in to reply.
No comments yet.