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 8/11
71.
closed
imp_refl
Implication is reflexive
theorem imp_refl (p : Prop ) : p → p := id
posted about 1 month ago
· proven 20 days ago
72.
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
73.
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
74.
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
75.
closed
fund_theorem_algebra
Fundamental theorem of algebra
theorem fund_theorem_algebra (p : Polynomial ℂ ) (h : 0 < p.degree) : ∃ z, p.eval z = 0 := by rcases Complex.exists_root h with ⟨z, hz⟩ exact ⟨z, hz⟩
posted about 1 month ago
· proven 20 days ago
76.
closed
prime_factorization_exists
Fundamental theorem of arithmetic (existence)
theorem prime_factorization_exists (n : Nat ) (h : 1 < n) : ∃ l : List Nat , (∀ p ∈ l, Nat .Prime p) ∧ l.prod = n := by use n.primeFactorsList refine ⟨fun p hp => Nat.prime_of_mem_primeFactorsLi...
posted about 1 month ago
· proven 20 days ago
77.
closed
gauss_sum
Sum of the first n naturals
theorem gauss_sum (n : Nat ) : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) := by rw [mul_comm 2] rw [Finset.sum_range_id_mul_two (n + 1)] rw [Nat.add_sub_c...
posted about 1 month ago
· proven 20 days ago
78.
closed
sqrt_two_irrational
Irrationality of √2
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by exact?
posted about 1 month ago
· proven 22 days ago
79.
closed
pigeonhole
Pigeonhole principle
theorem pigeonhole {α β : Type } [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ a₁ a₂, a₁ ≠ a₂ ∧ f a₁ = f a₂ := Fintype.exists_ne_map_eq_of_card_lt f h
posted about 1 month ago
· proven 20 days ago
80.
closed
nat_even_or_odd
Every natural is even or odd
theorem nat_even_or_odd (n : Nat ) : (∃ k, n = 2 * k) ∨ (∃ k, n = 2 * k + 1) := by rcases Nat.even_or_odd n with h | h · left rcases h with ⟨k, rfl⟩ use k ri...
posted about 1 month ago
· proven 20 days ago