Submit a theorem you want proved. Pledge USDC as a reward. When someone submits a verified Lean 4 proof, they earn it.
Open theorems
12
of 105 total
Total theorems
105
submitted
Proofs verified
229
93 theorems closed
USDC pledged
$ 0.04
funded on Solana
§ Theorems · 105 entries · page 9/11
81.
closed
list_reverse_reverse
Reverse is an involution
theorem list_reverse_reverse {α : Type} (l : List α) : l.reverse.reverse = l := List.reverse_reverse l
posted about 1 month ago
· proven 20 days ago
82.
closed
list_length_append
Length distributes over append
theorem list_length_append {α : Type} (l₁ l₂ : List α) : (l₁ ++ l₂).length = l₁.length + l₂.length := List.length_append
posted about 1 month ago
· proven 20 days ago
83.
84.
85.
86.
closed
list_append_nil
Empty list is right identity for append
theorem list_append_nil {α : Type} (l : List α) : l ++ [] = l := List.rec rfl (fun x _ => congrArg (List.cons x)) l
posted about 1 month ago
· proven 21 days ago
87.
88.
closed
bool_not_not
Boolean double negation
theorem bool_not_not (b : Bool) : !!b = b := b.casesOn rfl rfl
posted about 1 month ago
· proven 21 days ago
89.
closed
nat_zero_add
Adding zero on the left
theorem nat_zero_add (n : Nat) : 0 + n = n := Nat.rec rfl (fun _ => congrArg Nat.succ) n
posted about 1 month ago
· proven 21 days ago
90.
closed
nat_add_zero
Adding zero on the right
theorem nat_add_zero (n : Nat) : n + 0 = n := rfl
posted about 1 month ago
· proven 21 days ago