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

theorem isWeakGiuga_iff_prime_dvd {n : ℕ} (hn : n.Composite) : IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ (n / p - 1)

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

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

theorem carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ (10 ^ 10)) : CarmichaelTotientFor n

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)

theorem GromovPolynomialGrowthTheorem [Group.FG G] : HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G

theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] : answer(False) ↔ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ

theorem jacobson_conjecture_of_right_noetherian : answer(False) ↔ ∀ (R : Type) [Ring R] [IsRightNoetherianRing R], JacobsonConjectureFor R

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

theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] : IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G)

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

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)

theorem snake_small_dimensions : map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98]

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

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 σ : ℝ)

theorem squarefree_of_isCarmichael {a : ℕ} (ha₁ : a.Composite) (ha₂ : IsCarmichael a) : Squarefree a

theorem flt_of_beal_conjecture (H : bealConjecture) : FermatLastTheorem

theorem carmichealTotientFor_odd {n : ℕ} (hn : Odd n) : CarmichaelTotientFor n

theorem not_congruentNumber_1 : ¬ congruentNumber 1

theorem new_mersenne_conjecture_of_prime : (∀ p, p.Prime → Odd p → NewMersenneConjectureStatement p) → ∀ p, Odd p → NewMersenneConjectureStatement p

lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s

theorem isSurjunctive_of_finite (G : Type) [Group G] [Finite G] : IsSurjunctive G

theorem pellNumber_sq_add_pellNumber_succ_sq (n : ℕ) : pellNumber (2 * n + 1) = pellNumber n ^ 2 + pellNumber (n + 1) ^ 2

lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d

theorem jacobson_conjecture_of_comm_ring (R : Type u) [CommRing R] [IsNoetherianRing R] : JacobsonConjectureFor R

theorem ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ, ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2

theorem pollock_tetrahedral.ncard_exceptions : type_of% pollock_tetrahedral.salzer_levine ↔ NotSumOfFourTetrahedral.ncard = 241

theorem exists_not_hasResolution_of_not_perfectField (k : Type u) [Field k] (hk : ¬ PerfectField k) : ∃ (X : Scheme.{u}) (sX : X ⟶ Spec (.of k)), IsIntegral X ∧ LocallyOfFiniteType sX ∧ QuasiCompact sX ∧ IsSeparated sX ∧ topologicalKrullDim X = 0 ∧ ¬ Scheme.HasResolution sX

theorem card_heightLE_div_pow_five_div_six_tensto : atTop.Tendsto (fun H ↦ (heightLE H).ncard / (H : ℝ) ^ (5 / 6 : ℝ)) (𝓝 (2 ^ (4 / 3 : ℝ) * 3 ^ (-3 / 2 : ℝ) / (riemannZeta 10).re))

theorem wolstenholme_theorem (p : ℕ) (h : p > 3) (hp : Nat.Prime p) : (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 3]

lemma isCarmichael_561 : IsCarmichael 561

theorem buchi_false_M0 : ¬ IsBuchi 0

theorem carchimichealTotientFor_zero : ¬ CarmichaelTotientFor 0

theorem lebesgue_nagell_solution_pos_one (p : ℕ) (hodd : Odd p) : (1 : ℤ) ^ 2 - 2 = (-1 : ℤ) ^ p

theorem congruentNumber_5 : congruentNumber 5

lemma graceful_tree_one_vertex : let T : SimpleGraph Unit := ⊥ let m := T.edgeFinset.card ∃ f : Unit → ℕ, 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 growthFunction_not_polynomial_of_infinite [Infinite G] {S : Set G} (hS : S.Finite) (h : Subgroup.closure S = ⊤) {C : ℝ} (d : ℕ) : ∃ (n : ℕ), C * n ^ d < GrowthFunction S n

theorem isHadamard_equiv_isHadamard' (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : IsHadamard' M ↔ IsHadamard M

theorem elkies_bound (C : ℝ) : HallIneq C 2⁻¹ → C < 0.0215

theorem jacobian_conjecture_identity (H : JacobianConjectureProp k σ) : ∃ (G : RegularFunction k σ σ), G.comp (id k σ) = id k σ ∧ (id k σ).comp G = id k σ

theorem jugglerStep_36 : jugglerStep 36 = 6

theorem hasLocalUniformization_top {F : Type*} [Field F] {k : Type*} [Field k] [Algebra k F] (A : Subalgebra k F) [Algebra.FiniteType k A] [IsFractionRing A F] : (⊤ : ValuationSubring F).HasLocalUniformization k

theorem rev10_120 : rev10 120 = 21

theorem additionChainLength_first_values : [ℓ(1), ℓ(2), ℓ(3), ℓ(4), ℓ(5), ℓ(6), ℓ(7), ℓ(8), ℓ(9), ℓ(10)] = [0, 1, 2, 2, 3, 3, 4, 3, 4, 4]

theorem snake_zero_zero : LongestSnakeInTheBox 0 = 0