Pick one.

theorem P_ne_NP : P ≠ NP

theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0) (u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionDecay u₀) : ∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ (f := 0) v p

theorem riemannHypothesis : RiemannHypothesis

theorem erdos_101 : (fun n => (numLinesWithFourPointMax n : ℝ)) =o[atTop] (fun n => (n : ℝ)^2)

theorem erdos_1020 (r : ℕ) (hr : 3 ≤ r) (n k : ℕ) (hk : 0 < k) (hrk : r * k - 1 ≤ n) : f n r k = max ((r * k - 1).choose r) (n.choose r - (n - k + 1).choose r)

theorem erdos_1029 : Tendsto (fun k : ℕ ↦ (SimpleGraph.diagonalRamsey k : ℝ) / ((k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2))) atTop atTop

theorem erdos_1030 : ∃ c > (0 : ℝ), ∃ L : ℝ, Tendsto (fun k : ℕ ↦ (SimpleGraph.classicalRamsey (k + 1) k : ℝ) / (SimpleGraph.classicalRamsey k k : ℝ)) atTop (nhds L) ∧ L > 1 + c

theorem erdos_104 : (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2)

theorem erdos_1107 : ∀ r ≥ 2, ∀ᶠ n in atTop, SumOfRPowerful r n

theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => (n α : Cardinal.{u}) + 1) → cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u}))

theorem erdos_159 : ∃ (c : ℝ) (_ : 0 < c) (C : ℝ), ∀ (n : ℕ), 1 ≤ n → (SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4) (SimpleGraph.completeGraph (Fin n)) : ℝ) ≤ C * (n : ℝ) ^ (2 - c)

theorem erdos_233 : (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^2

theorem erdos_236: (fun n => (f n : ℝ)) =o[atTop] (fun n => Real.log (n : ℝ))

theorem erdos_242 (n : ℕ) (hn : 2 < n) : ∃ x y z : ℕ, 1 ≤ x ∧ x < y ∧ y < z ∧ (4 / n : ℚ) = 1 / x + 1 / y + 1 / z

theorem erdos_243 (a : ℕ → ℕ) (ha₀ : StrictMono a) (ha₁ : Tendsto (fun n ↦ (a n : ℝ) / a (n - 1) ^ 2) atTop (𝓝 1)) (ha₂ : Summable ((1 : ℚ) / a ·)) : ∀ᶠ n in atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

theorem erdos_282 {x : ℚ} (hx : x ∈ Set.Ioo 0 1) (hx_den : Odd x.den) : greedyUnitFractionRem { n | Odd n } x =ᶠ[atTop] 0

theorem erdos_364 : ¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2)

theorem erdos_371 : { n | Nat.maxPrimeFac (n + 1) > Nat.maxPrimeFac n }.HasDensity (1/2)

theorem erdos_373 : S.Finite

theorem erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) : Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ)^(1/3 : ℝ)) = 0

theorem erdos_535 : ∀ r ≥ 3, ∃ c > (0 : ℝ), ∀ᶠ (N : ℕ) in atTop, (f r N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ)))

theorem erdos_563 : ∀ (α : ℝ), 0 ≤ α → α < 1 / 2 → ∃ (c : ℝ), 0 < c ∧ Tendsto (fun n : ℕ => (F n α : ℝ) / Real.log n) atTop (nhds c)

theorem erdos_572 (k : ℕ) (hk : 3 ≤ k) : ∃ c > (0 : ℝ), ∀ᶠ (n : ℕ) in atTop, c * (n : ℝ) ^ (1 + 1 / (k : ℝ)) ≤ (SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph (2 * k)) : ℝ)

theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) : ∃ D : Finset G.Subgraph, (∀ H ∈ D, IsPathSubgraph H) ∧ IsDecomposition G D ∧ D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊

theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V] (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) : ∃ (S : Finset V) (k : Fin r), S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

theorem erdos_779 (n : ℕ) (hn : n ≥ 1): let P := ∏ i ∈ range (n + 1), nth Nat.Prime i ∃ p, p.Prime ∧ (P + p).Prime ∧ nth Nat.Prime n < p ∧ p < P

theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop

theorem erdos_859 : ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧ (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂)

theorem erdos_89 : (fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop] (fun n => (minimalDistinctDistances ℝ² n : ℝ))

theorem erdos_982 (n : ℕ) (hn : 3 ≤ n) (p : Fin n → ℝ²) (hp : Function.Injective p) (hp' : EuclideanGeometry.IsConvexPolygon p) : ∃ (i : Fin n), { d : ℝ | ∃ j : Fin n, j ≠ i ∧ d = dist (p i) (p j) }.ncard ≥ n / 2

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