Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 126

claims/: The 2 claim pages of Problem 126, one per claimant's result; the problem's standing derives from them.

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

Status. PROVED (LEAN), the site's label, crediting GPT-6 Astra; the compared Lean proves $f(n)/\log n\to\infty$ , and an alternate module of the same repository gives $f(n)\gg n^{1/2}$ . The claim pages, both of that square-root bound, are Adamczewski 2026 (the Lean proof found by a pre-release GPT-6 Astra in Epoch AI's benchmark run, published in Tom Adamczewski's repository) and JohnVictor36 2026 (a Lean repository with a draft write-up). See Current assessment for the evidence.

Source. erdosproblems.com/126, accessed 2026-09-05. Cite as: T. F. Bloom, Erdős Problem #126, https://www.erdosproblems.com/126.

References.

[ErTu34] Erdős, Paul and Turan, Paul, On a Problem in the Elementary Theory of Numbers. Amer. Math. Monthly (1934), 608-611.

Formalization. The statement file ErdosProblems/126.lean of formal-conjectures (pinned at its commit of 2026-09-18) states the question as erdos_126, answer(True), category research solved, with a sorry body and a formal_proof attribute naming line 3053 of the module Erdos126/Resolutions/Erdos126_132usd_25h.lean of the proof repository at a pinned commit; its variant erdos_126.variants.IsBigO (the Erdős–Turán bounds) is marked solved and erdos_126.variants.isLittleO ( $f(n)=o(n/\log n)$ ) open. This corpus built the proof repository at that pinned commit, checked the axioms of the compared declaration in the primary module and in each of the three alternates, and found its fingerprint identical to the comparator challenge in all four, as the claim page records; the repository's public CI reported the same comparison for the limit statement on the pinned commit. The compared declaration is the limit statement; the square-root bound is formally checked, without a challenge, in the alternate module Erdos126_104usd_15h. See the source digest for the different scopes of the primary and alternate modules.

Current assessment

The standing is solved through one accepted full claim; the second claim of the square-root bound is pending. Adamczewski 2026 is the Lean proof found by a pre-release GPT-6 Astra in Epoch AI's FrontierMath Erdős run and published in Tom Adamczewski's repository, and is accepted on formalized evidence: this corpus built the repository at its pinned commit, found the axioms of the compared declaration to be the three standard ones in the primary module and in each alternate, matched its fingerprint to the comparator challenge that pins it and audited its statement clause by clause against the Statement above, as the claim page records. The site's curator registered it as a proof claim on the site's proof-claims tab on 2026-09-03 and co-authored the paper that announces it (arXiv:2609.25050, a preprint), so his label and credit are not an independent review of a proof claim he submitted and no reviewed evidence is listed; the exposition is a placeholder that GPT generated from the Lean proof at the curator's request, so there is no refereed write-up. The compared declaration is the limit statement $f(n)/\log n\to\infty$ ; the square-root bound is formally checked in the alternate module Erdos126_104usd_15h, which no challenge compares, and is not asserted to be optimal. JohnVictor36 2026 is a Lean repository whose commits are dated 2026-09-02 and 2026-09-03, registered on the site on 2026-09-04, asserting at least $\sqrt{n/12}$ distinct prime factors; it holds a draft write-up and a README reporting a clean build with only the three standard axioms and the bound $|A|\le13r^2$ , and a comment of 2026-09-05 on the claim's panel reports that it compiles, but no review of its mathematics is recorded, as the source digest also notes. Neither claim has a refereed write-up, and no priority between the two is determined. The library's result pages for the GPT-6 Astra exposition state its results with proof sketches, claims checked against the print; they award no acceptance, and no independent review of them is recorded.

Progress

The [[../library/arithmetic_functions/erdos_1934_problem_elementary_theory_numbers/_index|Erdős–Turán paper]] is the historical source. The site attributes the earlier bounds $\log n\ll f(n)\ll n/\log n$ to it; the library holds no compilation of those historical proofs.

On 2026-09-03, Thomas F. Bloom registered the GPT-6 Astra result as a proof claim on the site's proof-claims tab, linking the public formal proofs and a preliminary exposition; the claim page Adamczewski 2026 records its standing. The [[../library/arithmetic_functions/adamczewski_2026_erdos126/main_theorem|two-copy argument]] gives $f(n)\gg\sqrt n$ by bounding the size of a set of at least two positive integers with $r$ supporting primes by $3r^2$ .

The method combines prime-power residue classes, a signed laminar-family estimate, and a matching into two copies of the vertex set. A logarithmic kernel supplies the needed conditional negativity. The source preserves other proof modules using different quantitative estimates; their differences and complete arguments are not recorded on this page.

Known Results

[[../library/arithmetic_functions/adamczewski_2026_erdos126/main_theorem|Quadratic prime-support bound]]: every finite $A\subseteq\mathbb N_0$ satisfies $|A|\leq3|S(A)|^2+2$ , where $S(A)$ is the prime support of its off-diagonal pair sums. Thus $f(n)\geq\sqrt{(n-2)/3}$ for $n\geq3$ , and the requested limit follows.
[[../library/arithmetic_functions/adamczewski_2026_erdos126/proposition_1|Signed laminar bound]]: the abstract estimate $n\leq3r^2$ , with a proof sketch and its same-source matching and kernel dependencies.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (29)

GPT-6 Astra square-root bound JohnVictor36 square-root bound problems/arithmetic_functions/E0126/claims Arithmetic Functions Arithmetic Functions arithmetic_functions/adamczewski_2026_erdos126 Conditional negativity of the logarithmic sum kernel The quadratic prime-support bound Proposition 1 — the signed laminar bound Two-copy matching for a laminar family arithmetic_functions/erdos_1934_problem_elementary_theory_numbers Conjecture (p. 609): n(k) = O(k^(1+eps)) for every eps > 0 Theorem I: 3 . 2^(k-1) positive integers always have a pairwise sum with a prime factor outside k given primes arithmetic_functions/erdos_1988_diophantine_equations_many_solutions Theorem 1 (p. 39): k integers and l shifts whose k l sums all have greatest prime factor below ((1+eps)(log k / l) log(log k / l))^l arithmetic_functions/gyory_1986_prime_factors_sums_integers_i Theorem 1 (p. 81): for finite sets |A| >= |B| >= 2 of positive integers, the product of the sums a + b has more than C_4 log |A| distinct prime factors arithmetic_functions/ha_2019_many_solutions_s_unit_equation_1 Theorem 1 (p. 2): sets of s primes with many solutions of a + 1 = c arithmetic_functions/konyagin_2007_two_s_unit_equations_many_solutions Theorem 2 (p. 1): arbitrarily large sets S of s primes with at least exp(s^{1/16}) solutions of a + 1 = c, and arbitrarily large N with #{d : d(d+1) | N} >= exp((log N)^{1/16})Hall (1935): On representatives of subsets Finite indexed representatives and partition conventions Elementary inputs and historical proof boundaries König's theorem (pp. 26, 30): equal finite blocks Lemma (pp. 27–28): the forced representative intersection Theorem 1 (p. 27): distinct representatives for a finite indexed family Theorem 2 (p. 29): representatives in different partition classes Theorem 3 (pp. 29–30): a common representative set for two partitions

Graph