---

The claim, registered on the site's proof-claims page on 2026-09-04 by the user JohnVictor36: $f(n)=\Omega(\sqrt n)$, and in the repository's statement every $A\subseteq\mathbb Z^{+}$ with $|A|=n\ge2$ has at least $\sqrt{n/12}$ distinct primes dividing $\prod_{a\ne b\in A}(a+b)$, which would answer Problem 126 affirmatively. In the claimant's outline the argument is by contradiction: one seeks a subset $B\subseteq A$ whose product of pairwise differences is at least its product of pairwise sums, after dividing out the common factors $\gcd(u,v)$ on both sides. For each prime $p$ the $p$-adic valuations of the two products differ by at most the contribution of one matching on $B$; a suitable $B$ and prime $p$ then give a slack of about a $1/r$ power of the whole product, while each matching recovers only about a $1/k$ power, which is the contradiction; the summary leaves $r$ and $k$ undefined. The repository, pinned above, holds a written proof, A Square-Root Lower Bound for Prime Divisors of Pairwise Sums (a working draft dated September 2026, the preprint link above, added on 2026-09-02 and revised on 2026-09-03), the Lean sources, committed on 2026-09-02 and 2026-09-03, and two README files. The top-level README says the code was generated by ChatGPT 5.6 Sol Ultra from a proof combining ideas of the author and that system (the site's claim line says the proof used communication with AI); the Lean README reports that the dependency chain compiles without sorry, admit, native_decide or custom axioms, that #print axioms gives only propext, Classical.choice and Quot.sound, and that its final bound is $|A|\le13r^2$ for $|A|>2$, where $r$ is the number of primes dividing the pairwise sums. The page is named by the site registration of 2026-09-04, the first public posting on record: the repository's commit dates of 2026-09-02 and 2026-09-03 show when its files were written, not when the repository became public, and the formalization link's date is that of the pinned commit.

Submission note. Posted to erdosproblems.com as a proof claim by JohnVictor36 (account JohnVictor36) on 4 September 2026, giving "communication with AI, giving the essential steps and asking AI for a detail implementation" as the AI used:

We proved that $f(n) =\Omega(\sqrt n)$. Our proof tries to derive a contradiction by finding a subset $B$ of $A$ such that $\prod\limits_{u\neq v \in B}|u-v|\geq \prod\limits_{u \neq v \in B}(u+v)$. The first essential observation is that when we look at each prime $p$, the $\nu_p$ of both sides differs by at most a matching: for any $B$, we can find a matching $M$ on $B$ such that $\nu_p(\prod\limits_{u\neq v \in B}|u-v|)\geq \nu_p(\prod\limits_{u \neq v \in B,(u,v) \notin M}(u+v))$. In this way, we can find some $B$ and a specific prime $p$ such that the slack created by that $p$ in the set $B$ is considerably large (at least $\Omega(\frac 1r)$-th power of the whole product), and then finish by showing that each matching only earns back $O(\frac 1k)$-th power. For the details, we need to actually remove $\gcd(u,v)$ from both sides to make the accounting correct. Notes: This proof is actually earlier than the one claimed by GPT astra, by looking at the github timestamps.

Depends on. Nothing in this wiki.

Standing. Claimed, not accepted. On the claim's comment panel, Johan Land reported on 2026-09-05 that the development compiles cleanly and that its formalization is the same as the formal-conjectures statement. That report and the README's own build and axiom list are third-party builds of Lean that this corpus has not built or audited, so they give no formalized evidence, and neither is a review of the mathematics; no independent review and no acceptance by the site's curator is recorded, and the draft write-up is unrefereed, so no reviewed or refereed evidence is listed either. The claim is separate from the GPT-6 Astra claim of the same bound, which the site credits, and the source card adamczewski_2026_erdos126 notes this one as pending. The claimant's note on the site asserts priority over the GPT-6 Astra claim by the repository's timestamps; upload dates alone do not establish priority or independence.