---

Claim. Shisheng Li and Zhong Zhuang, Coprime pairs with equal sum of divisors, assuming smooth shifted primes, a four-page draft in the authors' repository, posted there under both names on 7 October 2026 (the first preprint link, whose PDF prints the date 8 October 2026) and revised on 11 October 2026 (the second, pinned to the commit the registry entry archives). The two versions state the same definition and theorems, and this page was read against the second. Write $P^+(m)$ for the largest prime factor of $m$. Definition 1.2 of the draft (p. 1) states Hypothesis $\mathrm{A}^+$: for every $0<\delta<1/4$ and every $\eta>0$ there is $y_0\ge1$ such that every real $y\ge y_0$ has

$$\#\{p\text{ prime}:\ p\le5y,\ P^+(p+1)\le y^\delta\}\ge y^{1-\eta}.$$

Its Theorem 1.3 (p. 1): if $\mathrm{A}^+$ holds, then for every $\varepsilon>0$, $h(x)>x^{2-\varepsilon}$ for all sufficiently large $x$, and the pairs may be taken squarefree. With the $h(x)$ of Problem 824, this is the problem's question answered yes under $\mathrm{A}^+$. The proof (Section 3, pp. 2--3) is Pollack and Pomerance's argument for their [[../library/arithmetic_functions/pollack_2016_problems_erdos_sum_divisors_function/theorem_p24|exponent $1.4$]], with the smoothness exponent sent to zero: with $y=(\log x)^B$, $B\ge8/\varepsilon$ and $\delta=1/(2B)$, products of about $\log x/(B\log\log x)$ distinct primes $p\le5y$ with $P^+(p+1)\le y^\delta$ are squarefree integers below $x$ whose values of $\sigma$ are $\sqrt{\log x}$-smooth; there are few such values, so Cauchy's inequality gives many pairs with equal $\sigma$, and removing the common factor of a pair that shares few primes leaves a coprime pair. The lower bound, without the squarefree addendum, is proved in Lean for natural $x$ (Section 4, p. 3), and Remark 3.1 (p. 3) extends it to real $x$ through $h(x)=h(\lceil x\rceil)$.

Theorem 1.4 of the draft (p. 2) assumes that the argument by which OpenAI's manuscript Weighted dilation graphs, smooth shifted primes and totient fibers (24 September 2026) proves its Theorem 1.2 is correct, and states that the same argument, modified as in Section 2, gives at least $x^{1-o(1)}$ primes $p$ with $2x-2<p\le5x$ and $P^+(p+1)\le x^\delta$ for every fixed $0<\delta<1/4$, so that $\mathrm{A}^+$ holds; Corollary 1.5 concludes that $h(x)=x^{2-o(1)}$ if that argument is correct. Section 2 (p. 2) gives the modification: the manuscript detects primes $2u+1$ with $u$ smooth, and the draft detects primes $2u-1$ instead, so that $p+1=2u$ is smooth. The manuscript's Sections 2--5 are used as stated, and in its Sections 6--7, the Type II estimate and the extraction of primes, $2u+1$ becomes $2u-1$. The one step the authors call more than notational is the determinant parametrization of the Type II estimate: from $mn=2eh-1$ and $m'n=2eh'-1$ with $m\ne m'$ they take $m'-m=-2ek$ and $h'-h=-kn$, so that $mh'-m'h=k$ and the shifted endpoints are again $z=m'h$ and $z+k=mh'$, which the manuscript's shift-cancellation theorem (its Theorem 5.1, for every $0<|k|\le(\log x)^C$) covers. Section 5 (p. 4) says the authors rechecked the manuscript's Sections 6--7 for the change of sign and have not verified its Sections 3--5. The version of 7 October also listed there, without assessing them, points that writing Lean statements for the manuscript had found underspecified, among them the hypothesis $\ell\ge1$, used but not stated in its definition of prime groups, and a coefficient form of its Theorem 4.1 that, the draft said, the theorem does not state. The version of 11 October keeps only the first, as a clarification that does not obstruct the application, which takes $\ell=1$.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-11-000021, version 1, registered on 11 October 2026 by its maintainers Shisheng Li and Zhong Zhuang:

A Lean formalization of the conditional lower bound for the number h(x) of pairs of coprime positive integers a < b < x with equal sums of divisors. Assuming Hypothesis A⁺, which supplies sufficiently many primes p with smooth p+1, h(x) exceeds x^(2-ε) for every ε > 0 and all sufficiently large natural x. The argument adapts Pollack and Pomerance's finite counting method. A⁺ itself, the squarefree strengthening, and the accompanying paper's argument relying on the WD preprint are not formalized here.

Covers. The whole question of Problem 824, answered yes, conditionally on Hypothesis $\mathrm{A}^+$. Accepted, the claim would establish the implication from $\mathrm{A}^+$, not the answer, and the problem would stay open until $\mathrm{A}^+$ is proved.

Depends on. Hypothesis $\mathrm{A}^+$, stated above, which is unproved and which no page of this wiki proves. The implication from $\mathrm{A}^+$ uses neither the OpenAI manuscript nor any claim on Problem 821; the draft's route to $\mathrm{A}^+$ is described under Hypothesis below.

Hypothesis. $\mathrm{A}^+$ asks, for every fixed $\delta\in(0,1/4)$, for $y^{1-o(1)}$ primes up to $5y$ whose successor has no prime factor above $y^\delta$. Unconditionally, the case $a=-1$ of Lichtman's Theorem 1.1 reaches only smoothness exponents above $15/(32\sqrt e)=0.2843\ldots$, outside the range $\mathrm{A}^+$ asks for. The draft's route to $\mathrm{A}^+$, its Theorem 1.4, is the argument of OpenAI's pending claim on Problem 821 for the manuscript's Theorem 1.2, the count of primes with smooth predecessors, rerun for primes with smooth successors. The manuscript states only the predecessor form, $P^+(p-1)\le x^\delta$, so its Theorem 1.2 does not imply $\mathrm{A}^+$ as stated: what would transfer is its proof, rerun for primes $2u-1$, an argument the draft describes in two paragraphs rather than writes out. This page's reading of the manuscript's Sections 6--7, in the library's transcription, finds the sign entering where the draft says and the counts unchanged at each place: the determinant identity, whose converse becomes $m(h'-h)=-k(2eh-1)$ under the same coprimality of $m$ and $k$; the divisor sums with $\tau(2u-1)$ and $\tau(v+1)$, bounded by the same fixed divisor moments; the Type I distribution, where $2u-1\equiv0$ modulo an odd $d$ again fixes one unit class of $u$; the sieve for balanced composites, where $mn\equiv-1$ in place of $mn\equiv1$ modulo $D_1$ and modulo each banned prime has the same numbers of residue pairs; and the final count, where $u\mapsto2u-1$ is injective, the primes lie in $[2x-1,4x-1]$ and $P^+(p+1)=\max(2,P^+(u))\le x^\delta$. That is a reading of where the sign enters, not a check of the proofs. The manuscript's Sections 3--5, which carry its new transference and shift-cancellation method, do not involve the sign, and neither the authors nor this corpus has checked them.

Formalization. The registry replays a submitted proof in the Lean kernel and compares it with a challenge statement. Its entry records Lean v4.35.0-rc2, the Mathlib revision it pins, the permitted axioms propext, Quot.sound and Classical.choice, a 58-line challenge file importing only Mathlib, checks by two further kernels, and an automated review by a language model with a neutral outcome and no warnings. The challenge theorem Palomar824.main_result assumes Erdos824.SmoothSuccessorHypWeak, which is Definition 1.2 with the primes counted up to $\lfloor5y\rfloor$, and concludes that for every real $\varepsilon>0$ there is an $X$ with $x^{2-\varepsilon}<h(x)$ for every natural $x\ge X$, where Erdos824.h x counts the pairs $1\le a<b<x$ with $\gcd(a,b)=1$ and equal values of Mathlib's $\sigma_1$, the problem's count at natural $x$. The repository's README reports that #print axioms lists only the three permitted axioms and that the development contains no sorry. The two versions' acknowledgments both say that AI tools were used extensively, and they differ on how. The version of 7 October says that Claude (Anthropic) checked the adaptation of the manuscript to $p+1$ and wrote the text and the Lean formalization, that GPT models (OpenAI) were used to referee drafts, and that the authors have checked the arguments and take responsibility for them. The version of 11 October says instead that the project owner reports that ChatGPT (OpenAI) produced the Lean formalization, which has had no human mathematical review, and that Codex (OpenAI) adapted it to the current toolchain and the registry's format. This corpus has neither built nor audited the development, and no statement-fidelity review of its challenge file exists here, so it gives no formalized evidence; it proves the implication only, so even audited it would not settle the problem.

Standing. Claimed. The draft is not refereed and is not on arXiv; the registry's replay and model review are not a review of the mathematics; and the draft says that AI tools were used extensively and that the OpenAI manuscript it relies on is itself AI-generated. The repository's first drafts, also of 7 October 2026, name Li as the only author. The OpenAI manuscript is pending on its own page, with no outside review known, and the problem stays open: $\mathrm{A}^+$ is unproved.