Erdős Problem #126: prime divisors of pairwise sums

For $$f(n)=\min_{|A|=n}\left|\left\{p\text{ prime}:p\mid a+b\text{ for some distinct }a,b\in A\right\}\right|,$$ Astra formally proves $$\frac{f(n)}{\log n}\to\infty.$$ The repository contains substantially stronger proofs. In particular, one verified alternate resolution establishes $$n\le 3r^2,$$ where $r$ is the number of supporting primes, yielding $$f(n)\gg n^{1/2}.$$ Other independent resolutions give exponents $1/3$, $1/5$, and $1/8$. Thus the formal work goes well beyond the qualitative conjecture, although only the limit statement is the registered benchmark theorem.

For $$f(n)=\min_{|A|=n}\left|\left\{p\text{ prime}:p\mid a+b\text{ for some distinct }a,b\in A\right\}\right|,$$ Astra formally proves $$\frac{f(n)}{\log n}\to\infty.$$ The repository contains substantially stronger proofs. In particular, one verified alternate resolution establishes $$n\le 3r^2,$$ where $r$ is the number of supporting primes, yielding $$f(n)\gg n^{1/2}.$$ Other independent resolutions give exponents $1/3$, $1/5$, and $1/8$. Thus the formal work goes well beyond the qualitative conjecture, although only the limit statement is the registered benchmark theorem.