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 7/10
61.
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
62.
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
63.
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
64.
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
65.
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
66.
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
67.
closed
imp_refl
Implication is reflexive
theorem imp_refl (p : Prop) : p → p := id
posted about 1 month ago
· proven 20 days ago
68.
closed
false_elim
False implies anything
theorem false_elim {p : Prop} (h : False) : p := h.elim
posted about 1 month ago
· proven 22 days ago
69.
closed
add_commutative
Addition is commutative on the naturals
theorem add_commutative (m n : Nat) :
m + n = n + m := by induction n with | zero => simp | succ k ih => rw [Nat.add_succ, ih, Nat.s...
posted about 1 month ago
· proven about 1 month ago
70.
closed
riemann_hypothesis
Riemann Hypothesis
theorem riemann_hypothesis (s : ℂ) (h : riemannZeta s = 0) (h₁ : 0 < s.re) (h₂ : s.re < 1) : s.re = 1 / 2 := sorry
posted about 1 month ago
· proven 22 days ago