---

Claim. There is an explicit finite set $A_3$ of positive integers with no three-term arithmetic progression and $\sum_{a\in A_3}1/a>3.0085385$, and an explicit finite set $A_4$ with no four-term arithmetic progression and $\sum_{a\in A_4}1/a>4.439753474215620$; hence, for the function $f$ of Problem 169,

$$f(3)\ge3.0085385\qquad\text{and}\qquad f(4)\ge4.4397534742.$$

This is Theorem 1.1 of the manuscript Two explicit sets with large reciprocal sum and no 3-term or 4-term arithmetic progression, dated 3 October 2026 and signed Kiichi, Shiori and Rin, posted on the problem's thread on 26 September 2026 under the name Kiichi; the manuscript's Section 10 says that Shiori and Rin are instances of Claude (Anthropic) run as the coding agent Claude Code, and that Kiichi is the human author who set the task and is responsible for the note. The previous records, which the site credits, are $3.00849$ from the construction of Wróblewski ([Wr84] on the problem page) and $4.43975$ from Walker's Kempner set ([Wa25]), so the gains are about $4.9\times10^{-5}$ for $k=3$ and, for $k=4$, about $1.05\times10^{-7}$ over the reciprocal sum of Walker's set itself (about $4.43975337$, which the printed record $4.43975$ truncates), the measure the manuscript uses. Both sets have one shape: a self-similar head cut at a finite scale (Wróblewski's translate of the Szekeres set for $k=3$, Walker's base-$55$ Kempner set cut near $10^{30.35}$ for $k=4$), with Wróblewski's Behrend-type blocks glued on above it in stages chosen by dynamic programming over the logarithmic scale: $84$ stages under Wróblewski's window-separation condition for $k=3$, and $38$ stages for $k=4$ under a lemma of the manuscript that a $k$-progression-free head followed by $(k-1)$-progression-free blocks, each starting above twice the largest element before it, stays $k$-progression-free. The finer values $3.008538522178115$ and $\sum_{a\in A_4}1/a\in[4.4397534744963946,4.4397534745348559]$, and the bracketing of Walker's own sum, rest on exact integer arithmetic outside Lean, as the manuscript states.

Covers. Two numerical lower bounds, $f(3)\ge3.0085385$ and $f(4)\ge4.4397534742$, from two explicit finite sets. Not covered, as the claimants themselves state in their Section 8: any upper bound, the growth of $f(k)$ in $k$, the finiteness of $f(k)$ for every $k$ (recorded on the release's claim page), and the displayed limit question; no optimality of either construction is claimed.

Depends on. Wróblewski's set and Walker's set, whose heads and, for $k=3$, Behrend-type blocks the two constructions extend; the manuscript says its Lean development re-proves the progression-freeness and the sums it needs from them in general form, so the bounds do not rest on those pages' standing.

Formalization. The claimants' own Lean development, distributed as the bundle linked above with its axiom logs, states each bound as one theorem: APFree.BellmanRecord.erdos169_lower_3_0085385 (a finite set of naturals, three-progression-free as a set of integers, with reciprocal sum above $30085385/10^7$) and APFree.FourTermRecord.setA4_apfree_and_lower (the set setA4, four-progression-free, with reciprocal sum above $4439753474215620/10^{15}$), beside setA4_apfree_and_beats_walker for the weaker constant $4439753369254541/10^{15}$ that brackets Walker's sum. The manuscript says the proofs use no sorry and no native_decide, that #print axioms reports only propext, Classical.choice and Quot.sound, and that the stage-by-stage checks of the two constructions (chain959 and chain4) and the digit-set check behind Walker's set are kernel evaluations of Boolean checkers over the stage tables (decide +kernel), while the gluing lemmas are proved in general form. This corpus has not built or audited the development, and the link is the claimants' own formalization, so the page lists no formalized evidence.

Standing. Claimed. The manuscript is self-published on the claimants' website with no arXiv version or journal record, and its Section 8 says that no mathematician outside the authors has reviewed the mathematics, the code or the Lean development. The site's label is OPEN and its page (last edited 4 April 2026) credits the records of Wróblewski and Walker, so the curator records no acceptance. The bounds are proved lower bounds for two instances, $k=3$ and $k=4$, of the estimate the problem asks for and nothing of the limit question, so the problem stays open.