---

Claim. The first displayed assertion of Problem 143 is false: there is a countably infinite set $A\subset\mathbb{Q}\cap[2,\infty)$ with no finite accumulation point such that $\lvert ka-b\rvert\ge1$ for all distinct $a,b\in A$ and all integers $k\ge1$, while

$$\sum_{a\in A}\frac{1}{a\log a}=\infty.$$

This is Theorem 1.2 of Mattia Apicella's manuscript A rational counterexample to the reciprocal-logarithmic assertion in Erdős problem 143 (dated 2 October 2026, 15 pages, in the repository linked above at its pinned commit). Every point of $A$ lies within $\tfrac12 m^{-12}$ to the right of an integer $m$, and $A$ is the union of a nested sequence of finite sets $F_1\subset F_2\subset\cdots$ with $\sum_{a\in F_R}1/(a\log a)\ge R/576$. The manuscript's analytic input is a selection lemma (its Theorem 2.1): a periodic set of integers of density above $2/3$ contains, above any threshold, a finite primitive set of weight $\sum 1/(n\log n)$ above $1/6$, proved through Euler products of Dirichlet $L$-functions, character orthogonality and an Abel average over the level sets of $\Omega(n)$, which are primitive. The construction places each new block on a common grid $DN$ whose residue classes the earlier configuration excludes only in small proportion, perturbs the selected integers by a rational shift with a prime private to the block so that all earlier multiplier constraints survive, and repeats; each round keeps every earlier point and adds weight at least $1/576$. The author notes that the result is consistent with the logarithmic-density theorem of Koukoulopoulos, Lamzouri and Lichtman, the problem's other displayed assertion.

Submission note. Posted to erdosproblems.com as a proof claim by Mattia Apicella (account mapice) on 3 October 2026, giving "GPT 6 Astra" as the AI used:

A counterexample to the reciprocal-logarithmic assertion in #143: a countable rational set $A\subset[2,\infty)$ satisfies $|ka-b|\ge1$ for all ordered distinct pairs and all positive integers $k$, but $\sum_{a\in A}1/(a\log a)=\infty$. Abel averaging extracts arbitrarily distant finite primitive sets of weight $>1/6$ from fixed periodic sets of density $>2/3$. Private primes, product grids and residue filters permit nested rational blocks while preserving all previous multiplier constraints. Each round retains the old points and adds at least $1/576$ of weight; the nested union therefore diverges. The complete Lean project proves the closed real-domain theorem, extended nonnegative divergence and ordinary non-summability. It does not contradict the Koukoulopoulos-Lamzouri-Lichtman logarithmic-density theorem. Notes: Submitted for mathematical review. Author: Mattia Apicella. AI assistance was used in exploration, formalization and exposition. Independent expert review and external acceptance are pending. The supplied records document two local Lean verification runs and an audit of all 245 proved declarations using only propext, Classical.choice and Quot.sound. No new full Lean build was performed while preparing this submission. Frozen source commit: 0f4b96940c97c7e0c36d17b584ec2bf1d842c02a. Lean 4.24.0; mathlib f897ebcf72cd16f89ab4577d0c826cd14afaafc7. Reproduce with bash scripts/bootstrap.sh followed by bash scripts/verify.sh. The repository includes the English paper, all mathematical sources, proof guides and verification evidence. Its frozen deterministic ZIP has SHA-256 d4a8477e5122ad7f66584483b84a93b14af38b3a412c8b9378617b2c2137fec6.

Covers. The convergence assertion only: the answer to whether the hypothesis forces $\sum_{x\in A}1/(x\log x)<\infty$ is no. The claim does not bear on the $o(\log n)$ assertion, which [[problems/divisors/E0143/claims/2025_02_13_koukoulopoulos_lamzouri_lichtman|the pending logarithmic-density theorem]] settles in the affirmative, nor on the full density, which need not tend to $0$ (Besicovitch's primitive sets). The forum lists the claim as a full proof claim, and on the thread the author asked what was thought missing for a full solution; the manuscript's theorem addresses the convergence assertion, which this page records as the part the claim settles.

Formal verification by the author. The repository at the pinned commit holds a Lean 4.24.0 project against a pinned Mathlib revision, 55 modules in the namespace Erdos143. Its theorems mainConclusion_proved and strongConclusion_proved give the rational set with the separation inequalities for every ordered pair of distinct elements and every positive natural multiplier, infinite total weight, local finiteness and the near-integer bound; realConclusion_proved restates the result for a subset of $\mathbb{R}$ contained in $[2,\infty)$ with the weight sum equal to $\top$ in the extended nonnegative reals and the real-valued terms not summable. The author reports two local verification runs and an audit of all 245 proved declarations, which depend only on propext, Classical.choice and Quot.sound, with no sorry and no project axiom; the author also reports that no fresh full build was run while preparing the submission. None of this has been built or audited here, so no formalized evidence is listed, and the formal-conjectures statement file of the problem, whose second part asserts the summability this result denies, is a statement and not a proof.

Claimant and system. Mattia Apicella, posting under the forum account mapice, submitted the claim on 2026-10-03 and signs the manuscript alone; the forum's tab names GPT 6 Astra as the system used, and the repository says AI assistance was used in exploration, formalization and exposition while the formal-verification claims rest on checked Lean statements and the recorded evidence. The manuscript says that independent expert review of the formulation, of its correspondence to Erdős's question and of the exposition has not been completed, and claims no priority or publication.

Standing. The repository's two commits, which hold the manuscript, are dated 2 October 2026 (UTC), which dates this page; whether the repository was public that day is not established. The forum post followed, stamped 2026-10-03 00:00:29 by the site's clock, with the manuscript and the repository as its external links. On 2026-10-07 the claim carried three visible comments: after a deleted post, the author asked what was thought missing for a full solution; a forum commenter wrote on 2026-10-05 that the submission looked like a full solution; and a further commenter remarked that, together with the Koukoulopoulos--Lamzouri--Lichtman theorem and Haight's density result, the question's three aspects appeared settled. The site's curator has not commented, the problem's label is unchanged, the manuscript is not refereed and nobody has recorded accepting it, so the claim is claimed.