Theorem Marketplace

Theorem Details

-- Both the bounty and the submission should be valid Lean files
-- In the bounty, you can replace the entire proof (or anything else) with a sorry
-- In the submissions, all sorries should be defined

theorem debug (n : Nat) : n + 3 = n + 3 :=
  sorry

Bounty: 0.0005 ETH

Status: Closed

Proof

theorem debug (n : Nat) : n + 3 = n + 3 :=
  rfl

Back to Bounties

Theorem Details

-- Both the bounty and the submission should be valid Lean files -- In the bounty, you can replace the entire proof (or anything else) with a sorry -- In the submissions, all sorries should be defined theorem debug (n : Nat) : n + 3 = n + 3 := sorry

Proof