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 7/11
61.
closed
nat_lt_trans
Less-than is transitive on naturals
theorem nat_lt_trans {a b c : Nat} (h₁ : a < b) (h₂ : b < c) : a < c := Nat.lt_trans h₁ h₂
posted about 1 month ago
· proven 20 days ago
62.
63.
closed
nat_succ_injective
Successor is injective
theorem nat_succ_injective {m n : Nat} (h : m + 1 = n + 1) : m = n := Nat.succ.inj h
posted about 1 month ago
· proven 20 days ago
64.
closed
nat_mul_one
Multiplication by one
theorem nat_mul_one (n : Nat) : n * 1 = n := Nat.mul_one n
posted about 1 month ago
· proven 20 days ago
65.
closed
nat_mul_zero
Multiplication by zero
theorem nat_mul_zero (n : Nat) : n * 0 = 0 := Nat.mul_zero n
posted about 1 month ago
· proven 20 days ago
66.
closed
nat_succ_ne_zero
Successor of natural is non-zero
theorem nat_succ_ne_zero (n : Nat) : n + 1 ≠ 0 := Nat.succ_ne_zero n
posted about 1 month ago
· proven 20 days ago
67.
closed
uncurry
Uncurry
theorem uncurry {p q r : Prop} (h : p → q → r) : p ∧ q → r := fun ⟨hp, hq⟩ => h hp hq
posted about 1 month ago
· proven 20 days ago
68.
closed
curry
Curry
theorem curry {p q r : Prop} (h : p ∧ q → r) : p → q → r := fun hp hq => h ⟨hp, hq⟩
posted about 1 month ago
· proven 20 days ago
69.
closed
or_symm
Disjunction is symmetric
theorem or_symm {p q : Prop} (h : p ∨ q) : q ∨ p := Or.symm h
posted about 1 month ago
· proven 20 days ago
70.
closed
and_symm
Conjunction is symmetric
theorem and_symm {p q : Prop} (h : p ∧ q) : q ∧ p := ⟨h.2, h.1⟩
posted about 1 month ago
· proven 20 days ago