Erdős problem 126

Let $f(n)$ be maximal such that if $A\subseteq\mathbb{N}$ has $|A| = n$ then $\prod_{a\neq b\in A}(a + b)$ has at least $f(n)$ distinct prime factors. Is it true that $\frac{f(n)}{\log n} \to\infty$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

126.lean

Retained formal statement1 of 3

Let $f(n)$ be maximal such that if $A\subseteq\mathbb{N}$ has $|A| = n$ then $\prod_{a\neq b\in A}(a + b)$ has at least $f(n)$ distinct prime factors. Is it true that $\frac{f(n)}{\log n} \to\infty$ ?

FormalConjectures/ErdosProblems/126.leanErdos126.erdos_1263 linesExact file

1True ↔2  ∀ (f : ℕ → ℕ),3    Erdos126.IsMaximalAddFactorsCard f → Filter.Tendsto (fun n => ↑(f n) / Real.log ↑n) Filter.atTop Filter.atTop

OpenStatement only, no proof