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 6/10
51.
closed
bezout
Bezout's identity
theorem bezout (a b : ℤ ) (h : a ≠ 0 ∨ b ≠ 0) : ∃ x y : ℤ , a * x + b * y = Int.gcd a b := by have _ := h use Int.gcdA a b, Int.gcdB a b exact (Int.gcd_eq_gcd_ab a b).symm
posted about 1 month ago
· proven 20 days ago
52.
closed
triangle_ineq
Triangle inequality (real)
theorem triangle_ineq (a b : ℝ ) : |a + b| ≤ |a| + |b| := abs_add_le a b
posted about 1 month ago
· proven 20 days ago
53.
closed
cauchy_schwarz_real
Schwarz inequality (real)
theorem cauchy_schwarz_real {n : ℕ } (x y : Fin n → ℝ ) : (∑ i, x i * y i) ^ 2 ≤ (∑ i, x i ^ 2) * (∑ i, y i ^ 2) := Finset.sum_mul_sq_le_sq_mul_sq Finset.univ x y
posted about 1 month ago
· proven 20 days ago
54.
closed
bool_and_comm
Boolean and is commutative
theorem bool_and_comm (a b : Bool) : (a && b) = (b && a) := by cases a <;> cases b <;> rfl
posted about 1 month ago
· proven 20 days ago
55.
closed
option_map_some
Option map of some
theorem option_map_some {α β : Type } (f : α → β) (a : α) : (Option.some a).map f = Option.some (f a) := rfl
posted about 1 month ago
· proven 20 days ago
56.
closed
list_length_map
List map preserves length
theorem list_length_map {α β : Type } (f : α → β) (l : List α) : (l.map f).length = l.length := List.length_map f
posted about 1 month ago
· proven 20 days ago
57.
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
58.
59.
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
60.
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