λleanlab

Proofs

An unfinished proof: sorry

See the warning for an admitted statement, then replace the placeholder.

Open Sorry.lean in editor

This example intentionally contains sorry. Replace it to complete the proof.

-- This file intentionally has an unfinished proof.
-- Check it: Problems reports "declaration uses 'sorry'".
theorem unfinished : 2 + 2 = 4 := by
  sorry

-- This calculation works even though the proof is unfinished.
#eval 2 + 2

-- Replace sorry with rfl and check again.
-- sorry can even admit a false statement: it is not evidence.

Explanation

sorry

Temporarily admits a claim and produces a warning. The file can elaborate, but its proof is unfinished. leanlab marks it Incomplete and does not award lesson completion.

#eval 2 + 2

This independent calculation still prints 4. Successful execution does not fill the missing proof.

Expected output

Reference only. Run the file to check its actual result.

4

Exercise

Replace sorry with rfl. The warning and Incomplete status should disappear.

Related examples