Pick one.

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 erdos_194 : answer(False) ↔ ∀ k ≥ 3, ∀ r : ℝ → ℝ → Prop, IsStrictTotalOrder ℝ r → ∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Pairwise r ∨ s.Pairwise (flip r))

theorem erdos_275 (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ) (H : ∃ k : ℤ, ∀ x ∈ Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD n i]) (x : ℤ) : ∃ i, x ≡ a i [ZMOD n i]

theorem erdos_277 : answer(True) ↔ ∀ c : ℝ, ∃ n : ℕ, (σ 1 n : ℝ) > c * n ∧ ∀ (m : StrictCoveringSystem ℤ), ∃ i, (n : ℤ) ∉ m.moduli i

theorem erdos_31 : ∀ A : Set ℕ, A.Infinite → ∃ B : Set ℕ, B.HasDensity 0 ∧ ∀ᶠ n in atTop, n ∈ A + B

theorem erdos_437 : answer(True) ↔ ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (1 - ε) < L x

theorem erdos_438 : Tendsto (fun N : ℕ ↦ (extremalSize N : ℝ) / (N : ℝ)) atTop (𝓝 ((11 : ℝ) / 32))

theorem erdos_482 : (∀ n : ℕ, 1 ≤ n → (a (2 * n + 1) : ℤ) - 2 * a (2 * n - 1) = (Real.digits (√2 / 2) 2 (n - 1) : ℕ)) ∧ Real.ofDigits (Real.digits (√2 / 2) 2) = √2 / 2

theorem erdos_484 : ∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 0 < k → ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ f : ℕ → Fin k, c * N ≤ (((Finset.Icc 1 N).filter fun n => ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n).card : ℝ)

theorem erdos_519 : answer(True) ↔ ∃ c : ℝ, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k : Fin n, c < ‖powerSum z (k.val + 1)‖

theorem erdos_645 (c : ℕ → Bool) : ∃ x d, 0 < x ∧ x < d ∧ (∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C)

theorem erdos_646 : answer(True) ↔ ∀ S : Finset ℕ, (∀ p ∈ S, p.Prime) → {n : ℕ | ∀ p ∈ S, Even (padicValNat p (n !))}.Infinite

theorem erdos_690 : answer(False) ↔ ∀ k ≥ 1, ∀ d : ℕ → ℝ, (∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) → IsUnimodalOnPrimes d

theorem erdos_728 : answer(True) ↔ ∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C, ∃ a b n : ℕ, 0 < n ∧ ε * n < a ∧ ε * n < b ∧ a ! * b ! ∣ n ! * (a + b - n)! ∧ a + b > n + C * log n ∧ a + b < n + C' * log n

theorem lambert_series_eq_num_divisor_sum : ∀ t : ℚ, ∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1) = ∑' n : ℕ+, (n : ℕ).divisors.card / ((t : ℝ) ^ (n : ℕ))

theorem f_undefined_at_2 : f 2 = 0

theorem isGood_example : IsGood {p ^ 2 | (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : p.Prime)}

theorem factorial_isPractical (n : ℕ) : Nat.IsPractical n.factorial

theorem le_chromaticNumber : (n : ℕ∞) ≤ C.graph.chromaticNumber

lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k → ℕ), (∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1

lemma claim2_inequality : ∀ᶠ n in atTop, ∀ δ : (Fin n) → ℚ, δ '' Set.univ ⊆ {-1,0,1} → letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))| lhs ≠ 0 → lhs ≥ 1 / (Icc 1 n).lcm id

theorem exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A

theorem f_id : f id = fun n ↦ #{d ∈ n.divisors | Odd d}

theorem example_maximal_sidon : IsMaximalSidonSetIn {1, 2, 4} 4

theorem maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) : maxSidonSubsetCard (Icc 1 N) ≤ 2 * Real.sqrt N

theorem sum_factorial_inv_eq_geometric : let f (n k : ℕ) : ℝ := 1 / ((n + 2).factorial : ℝ) ^ (k + 1) ∑' n : ℕ, (1 : ℝ) / ((n + 2).factorial - 1) = ∑' n : ℕ, ∑' k : ℕ, f n k

theorem erdos_69 : Irrational <| ∑' n, ω (n + 2) / 2 ^ (n + 2)

theorem erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) : L n ≤ n - 1

theorem f_zero_eq : f 0 = 0

theorem two_not_mem_pillaiPrimes : ¬ 2 ∈ PillaiPrimes

theorem greedySidonSet_isSidon (n : ℕ) : IsSidon (Finset.greedySidonBelow n : Set ℕ)

theorem greedyUnitFractionRem_zero (n : ℕ) : greedyUnitFractionRem .univ (1 / n) 0 = 0

theorem erdos_287.test.best_possible : let s : Fin 3 → ℕ := ![2, 3, 6] StrictMono s ∧ 1 < s 0 ∧ ∑ i : Fin 3, 1 / (s i : ℝ) = 1 ∧ max_gap 3 s = 3

theorem M_one : M 1 = 1

theorem maxSubsetSumAvoidingCard_three_four : maxSubsetSumAvoidingCard 3 4 = 2

theorem exists_three_full_then_two_full : ∃ n > 0, (3).Full n ∧ (2).Full (n + 1)

theorem erdos_445.test.small_example : Erdos445Prop 1 5 1

theorem tauPlus_six : tauPlus 6 = 3

private lemma evens_infinite : Set.Infinite {n : ℕ | Even n}

theorem bookNumber_bot {n : ℕ} : bookNumber (⊥ : SimpleGraph (Fin n)) = 0

theorem unitDistanceCounts_BddAbove (n : ℕ) : BddAbove <| unitDistanceCounts n

theorem not_isCoprimePowerfulAP4_zero_one : ¬ IsCoprimePowerfulAP4 0 1