Fewest primes dividing all pairwise sums of an $n$-set: is $f(n)/\log n\to\infty$? (Erdős #126)

For a finite set $A\subseteq\mathbb{N}$, let $P(A)$ be the number of distinct primes dividing $\prod_{a\neq b\in A}(a+b)$, the product of all pairwise sums of distinct elements of $A$. Let $f(n)$ be the largest number such that every $A\subseteq\mathbb{N}$ with $\lvert A\rvert=n$ has $P(A)\ge f(n)$; equivalently, $f(n)=\min_{\lvert A\rvert=n}P(A)$ is the guaranteed minimum number of distinct prime factors among all pairwise sums. Is it true that $f(n)/\log n\to\infty$?

Acceptance. FULLY RESOLVES: a complete proof that $f(n)/\log n\to\infty$ (full written proof, Lean/Coq-checkable preferred) — OR a disproof: a proof that $f(n)\ll\log n$ (the ratio stays bounded), for instance an explicit infinite family of $n$-element sets $A_n$ whose pairwise sums together have $O(\log n)$ distinct prime factors, with proof. ADVANCES: improve the best-known lower bound on $f(n)$ strictly beyond the $\log n\ll f(n)$ stated in the background (any superlogarithmic lower bound, with proof); OR improve the upper bound below the trivial $\ll n/\log n$ by proving $f(n)=o(n/\log n)$, the specific gap Erdős highlights; OR compute exact certified values of $f(n)$ for a range of small $n$, delivered with the search code and, for each $n$, a proof that the minimising set is optimal, extending beyond any published table. Deliver the proof, or the improved-bound proof, or the exact-value search code with its per-$n$ optimality certificates.