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 · 93 entries · page 9/10
81.
82.
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
83.
84.
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
85.
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
86.
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
87.
closed
comp_apply
Function composition unfolds
theorem comp_apply {α β γ : Type} (f : β → γ) (g : α → β) (x : α) : (f ∘ g) x = f (g x) := rfl
posted about 1 month ago
· proven 21 days ago
88.
closed
modus_ponens
Modus ponens
theorem modus_ponens {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp
posted about 1 month ago
· proven 21 days ago
89.
closed
true_intro
True is true
theorem true_intro : True := trivial
posted about 1 month ago
· proven 21 days ago
90.
closed
or_self_idem
Disjunction is idempotent
theorem or_self_idem (p : Prop) : (p ∨ p) ↔ p := Iff.intro (fun h => h.elim id id) Or.inl
posted about 1 month ago
· proven 21 days ago