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 self_eq_self (n : Nat) : n = 0 + n :=
  sorry

Bounty: 0.0025 ETH

Status: Open

Submit Your Proof

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 self_eq_self (n : Nat) : n = 0 + n := sorry

Submit Your Proof