166 problems · 60 unsolved

Pick one.

Every statement is already formalized in Lean by formal-conjectures. Easy ones are warm-ups with known proofs. Unsolved ones are open research problems.

Unsolved60

PNP NS RH E101 E1020 E1029 E1030 E104 E1107 E1167 E159 E233 E236 E242 E243 E282 E364 E371 E373 E41 E535 E563 E572 E583 E617 E779 E82 E859 E89 E982 Ag Be Br Bc Ca Ct Co Ab Di Eu Fe Ga Gr Ha Hl In Ju Ku Kt La Le Lo Ln Mo Op RH₂ Pi Po Lv Va

Hard30

NS₂ Poi E194 E275 E277 E31 E437 E438 E482 E484 E519 E645 E646 E690 E728 Ao Bk Bo Cr El Go Ja Jc Lg Li Lc Pe Sn Ls Er

Medium38

Cm E1049 E1054 E12 E18 E19 E295 E317 E329 E358 E42 E44 E68 E69 E872 Do Ev Ee Gu Re Rv Ge Mi Ah Ba Ci Cn Au Cw Gt If Ii Jo Mv Pl Rs So Wo

Easy38

RH₃ E107 E1074 E156 E282₂ E287 E36 E361 E366 E445 E448 E602 E80 E90 E937 Ad Ai En Ey Fi Lt Th Tw AG Bh Cc Cl Cg Gc Gm Hd H Jb Jg Ll Ly Sc Sa

Open · sorry Known result Worker on it Proved here

15 shown

Agoh-Giuga conjecture
theorem isWeakGiuga_iff_prime_dvd {n : ℕ} (hn : n.Composite) : IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ (n / p - 1)
hard
Beck–Fiala theorem and conjecture
theorem beck_fiala_theorem (n m t : ℕ) (ht : 1 ≤ t) (S : Fin m → Finset (Fin n)) (hdeg : ∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) : ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧ ∀ i, |∑ j ∈ S i, χ j| ≤ 2 * (t : ℝ) - 1
hard
Brocard's Conjecture
theorem brocard_conjecture.ferreira_large_n : ∀ᶠ n in atTop, letI prev := n.nth Nat.Prime; letI next := (n+1).nth Nat.Prime; 4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card
hard
Carmichael's totient function conjecture
theorem carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ (10 ^ 10)) : CarmichaelTotientFor n
hard
Euler's sum of powers conjecture
theorem eulers_sum_of_powers_conjecture.false_for_k4 : ¬ (∀ (n b : ℕ) (_ : 1 < n) (a: Fin n → ℕ) (_ : ∀ i, a i > 0) (_ : ∑ i, (a i) ^ 4 = b ^ 4), 4 ≤ n)
hard
Gromov's theorem on groups of polynomial growth
theorem GromovPolynomialGrowthTheorem [Group.FG G] : HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G
hard
Jacobian conjecture
theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] : answer(False) ↔ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ
hard
Jacobson Conjecture
theorem jacobson_conjecture_of_right_noetherian : answer(False) ↔ ∀ (R : Type) [Ring R] [IsRightNoetherianRing R], JacobsonConjectureFor R
hard
Legendre's conjecture
theorem bounded_gap_legendre (H : ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)) : ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p
hard
Leinster Groups
theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] : IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G)
hard
Local uniformization
theorem local_uniformization_of_charZero (k F : Type*) [Field k] [Field F] [Algebra k F] [Algebra.EssFiniteType k F] [CharZero k] (𝒪 : ValuationSubring F) (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) : 𝒪.HasLocalUniformization k
hard
Pierce–Birkhoff conjecture
theorem pierce_birkhoff_conjecture_dim_one (f : ℝ → ℝ) (hf : IsPiecewisePolynomial f) : ∃ (ι κ : Type) (g : ι → κ → Polynomial ℝ), Finite ι ∧ Finite κ ∧ ∀ x, f x = ⨆ i, ⨅ j, Polynomial.eval x (g i j)
hard
Snake in the box
theorem snake_small_dimensions : map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98]
hard
The Lovász–Plummer conjecture (proved 2011) and Sheehan's conjecture
theorem lovasz_plummer_conjecture : ∃ c : ℝ, 0 < c ∧ ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], (∀ v, G.degree v = 3) → G.IsBridgeless → (2 : ℝ) ^ (c * Fintype.card V) ≤ perfectMatchingCount G
hard
Černý Conjecture
theorem shitov_upper_bound : ∃ f : ℝ → ℝ, f =o[atTop] (fun n : ℝ => n ^ 3) ∧ ∀ {α : Type*} {σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing) , ∃ w : List α, M.IsSynchronizingWord w ∧ (w.length : ℝ) ≤ (7 / 48 + 2 * 15625 / 1597536) * (Fintype.card σ : ℝ) ^ 3 + f (Fintype.card σ : ℝ)
hard