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 8/10
71.
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
72.
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
73.
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
74.
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
75.
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
76.
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
77.
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
78.
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
79.
80.