Pick one.

theorem agoh_giuga : AgohGiugaCongr

theorem beck_fiala_conjecture : ∃ C : ℝ, 0 < C ∧ ∀ (n m t : ℕ) (S : Fin m → Finset (Fin n)), (∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) → ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧ ∀ i, |∑ j ∈ S i, χ j| ≤ C * Real.sqrt t

theorem brocard_conjecture (n : ℕ) (hn : 1 ≤ n) : letI prev := n.nth Nat.Prime; letI next := (n+1).nth Nat.Prime; 4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card

theorem buchi_problem_M5 : IsBuchi 5

theorem charmichaelTotient : ∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotientFor n

theorem pillais_conjecture (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : { (x, y, m, n) : (ℕ × ℕ × ℕ × ℕ) | 1 < x ∧ 1 < y ∧ 1 < m ∧ 1 < n ∧ (m, n) ≠ (2, 2) ∧ a * x^n - b * y^m = c }.Finite

theorem Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) : 2 * (A n).ncard = (B n).ncard → congruentNumber n

theorem new_mersenne_conjecture (p : ℕ) (hp : Odd p) : NewMersenneConjectureStatement p

theorem dickson_conjecture (fs : Finset ℤ[X]) (hfs : ∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) (hfs' : SchinzelCondition fs) : Infinite {n : ℕ | ∀ f ∈ fs, (f.eval (n : ℤ)).natAbs.Prime}

theorem eulers_sum_of_powers_conjecture (n k b : ℕ) (hn : 1 < n) (hk : 5 < k) (a : Fin n → ℕ) (ha : ∀ i, a i > 0) (hsum : ∑ i, (a i) ^ k = b ^ k) : k ≤ n

theorem feit_thompson_primes (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : p < q) : ¬ (q ^ p - 1) / (q - 1) ∣ (p ^ q - 1) / (p - 1)

theorem gap_conjecture : ∀ (G : Type) [Group G] (S : Set G), S.Finite → Subgroup.closure S = ⊤ → HasSuperPolynomialGrowth G → ∃ C : ℕ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, Real.exp (Real.sqrt (n : ℝ)) ≤ (GrowthFunction S (C * n) : ℝ)

theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) : let m := T.edgeFinset.card ∃ f : V → ℕ, Function.Injective f ∧ (∀ v, f v ≤ m) ∧ T.edgeFinset.image (fun e => e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)), fun u v => by show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m

theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M

theorem hall_conjecture : HallConjectureExp 2⁻¹

theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p

theorem juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ m, jugglerStep^[m] n = 1

theorem kummer_vandiver (p : ℕ+) (hp : p.Prime) : ¬ ↑p ∣ (classNumber (maximalRealSubfield (CyclotomicField p ℚ)))

theorem KotheConjecture (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J)

theorem lander_parkin_selfridge : ∀ (k n m : ℕ) (x : Fin n → ℕ) (y : Fin m → ℕ), 0 < n → 0 < m → (∀ i, 0 < x i) → (∀ j, 0 < y j) → (∀ i j, x i ≠ y j) → ∑ i, x i ^ k = ∑ j, y j ^ k → k ≤ n + m

theorem lehmer_mahler_measure_problem : ∃ μ : ℝ, ∀ f : ℤ[X], μ > 1 ∧ (mahlerMeasureZ f > 1 → mahlerMeasureZ f ≥ μ)

theorem local_uniformization (k F : Type*) [Field k] [Field F] [Algebra k F] [Algebra.EssFiniteType k F] (p : ℕ) [Fact p.Prime] [CharP k p] (𝒪 : ValuationSubring F) (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) : 𝒪.HasLocalUniformization k

theorem lonely_runner_conjecture (n : ℕ) (speed : Fin n ↪ ℝ) (lonely : Fin n → ℝ → Prop) (lonely_def : ∀ r t, lonely r t ↔ ∀ r2 : Fin n, r2 ≠ r → dist (t * speed r : UnitAddCircle) (t * speed r2) ≥ 1 / n) (r : Fin n) : ∃ t ≥ 0, lonely r t

theorem volume_eq_sofaConstant_iff_congruent_gerversSofa (s : Set ℝ²) (hs : ∃ m, IsMovingSofa s m) : volume s = sofaConstant ↔ ∃ g : E(2), s = g '' gerversSofa

theorem n_dim_euler_brick_existence :

theorem irrational_seven : ∃ x, Irrational x ∧ riemannZeta 7 = x

theorem pierce_birkhoff_conjecture {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hf : IsPiecewiseMvPolynomial f) : ∃ (ι κ : Type) (g : ι → κ → MvPolynomial (Fin n) ℝ), Finite ι ∧ Finite κ ∧ ∀ x, f x = ⨆ i, ⨅ j, MvPolynomial.eval x (g i j)

theorem pollock_tetrahedral (N : ℕ) : ∃ f : Fin 5 → ℕ, N = ∑ i, tetrahedral (f i)

theorem sheehan_conjecture : ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], (∀ v, G.degree v = 4) → ∀ (v : V) (c : G.Walk v v), IsHamiltonianCycle G c → ∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧ c'.edges.toFinset ≠ c.edges.toFinset

theorem vaught_conjecture {L : FirstOrder.Language} (hL : Countable L.Symbols) {T : L.Theory} (hT : T.IsComplete) : numberOfCountableModels T ≤ Cardinal.aleph0 ∨ numberOfCountableModels T = Cardinal.continuum