theorems.fun
a working notebook of open problems ↘
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
status All 105 Open 12 Closed 93
sort Most reward Recent
§ Theorems · 93 entries · page 3/10
22.
closed false
False
theorem false : False := sorry
posted about 1 month ago · proven about 1 month ago
Rewards
no reward
View proof →
23.
closed googol_add_prime
Primality of 10^100 + 267
theorem googol_add_prime : ∀ a b, 1 < a → 1 < b → a * b ≠ (10 ^ 100 + 267) := sorry
posted about 1 month ago · proven about 1 month ago
Rewards
no reward
View proof →
24.
closed erdos_discrepancy
Erdős discrepancy problem
theorem erdos_discrepancy : ∀ (s : ℕ → ({-1, 1} : Set ℤ)), ∀ C : ℝ, ∃ d n : ℕ, 0 < d ∧ 0 < n ∧ C < |∑ k ∈ Finset.range n, (s (d * (k + 1)) : ℝ)| := sorry
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
25.
closed fermat_two_squares
Sum of two squares (Fermat)
theorem fermat_two_squares (p : ℕ) (hp : p.Prime) (h : p % 4 = 1) : ∃ a b : ℕ, p = a ^ 2 + b ^ 2 := sorry
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
26.
closed lagrange_four_squares
Lagrange four-square theorem
theorem lagrange_four_squares (n : ℕ) : ∃ a b c d : ℕ, n = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 := by obtain ⟨a, b, c, d, h⟩ := Nat.sum_four_squares n use a, b, c, d rw [h]
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
27.
closed sylow_one
Sylow's first theorem
theorem sylow_one {G : Type*} [Group G] [Fintype G] (p : ℕ) (hp : p.Prime) (n : ℕ) (h : p ^ n ∣ Fintype.card G) : ∃ H : Subgroup G, Nat.card H = p ^ n := by haveI : Fact p.Prime := ⟨hp⟩ rw [← Nat.card_eq_fintype_card] at h exact Sy...
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
28.
closed cayley_thm
Cayley's theorem
theorem cayley_thm {G : Type*} [Group G] : ∃ f : G →* Equiv.Perm G, Function.Injective f := ⟨{ toFun x := { toFun y := x * y invFun y := x⁻¹ * y left_inv y := inv_mul_ca...
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
29.
closed picard_little
Picard's little theorem
theorem picard_little (f : ℂ → ℂ) (hf : Differentiable ℂ f) (h : ¬ ∃ c, ∀ z, f z = c) : ∀ a b : ℂ, a ≠ b → (Set.range f)ᶜ ⊆ {a, b} := sorry
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →
30.
closed liouville_thm
Liouville's theorem (bounded entire is constant)
theorem liouville_thm (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hb : ∃ M, ∀ z, ‖f z‖ ≤ M) : ∃ c, ∀ z, f z = c := by apply hf.exists_const_forall_eq_of_bounded rw [isBounded_iff_forall_norm_l...
posted about 2 months ago · proven about 1 month ago
Rewards
no reward
View proof →