Erdős Problem 1106

Reference: erdosproblems.com/1064

def Erdos1106.p : ℕ → ℕ

The partition function p(n) is the number of ways to write n as a sum of positive integers (where the order of the summands does not matter).

Equations

• Erdos1106.p n = Fintype.card n.Partition

theorem Erdos1106.erdos_1106 : Filter.Tendsto (fun (n : ℕ) => (∏ i ∈ Finset.Icc 1 n, p i).primeFactors.card) Filter.atTop Filter.atTop

Let $p(n)$ be the partition number of $n$ and $F(n)$ be the number of distinct prime factors of $∏_{i= 1} ^ {n} p(n)$, then $F(n)$ tends to infinity when $n$ tends to infinity.

theorem Erdos1106.erdos_1106_k2 : ∀ᶠ (n : ℕ) in Filter.atTop, (∏ i ∈ Finset.Icc 1 n, p i).primeFactors.card > n

Let $p(n)$ be the partition number of $n$ and $F(n)$ be the number of distinct prime factors of $∏_{i= 1} ^ {n} p(n)$, $F(n)>n$ for sufficiently large $n$.