Wiki
Wiki

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

Updated


Kovač proves, as Theorem 1, that the set X⊆R3X\subseteq\mathbb R^3 of Problem 268, the triples

(∑n∈A1n, ∑n∈A1n+1, ∑n∈A1n+2)\Bigl(\sum_{n\in A}\frac1n,\ \sum_{n\in A}\frac1{n+1},\ \sum_{n\in A}\frac1{n+2}\Bigr)

over infinite A⊆NA\subseteq\mathbb N with ∑n∈A1/n<∞\sum_{n\in A}1/n<\infty, has nonempty interior, which is exactly the question's affirmative answer. The proof is constructive: after a linear change of variables the series becomes a perturbed vector series with leading terms (1/n,2/n2,2/n3)(1/n,2/n^2,2/n^3), and a convergence game played against the perturbation errors shows that every point of a small open ball is represented; Section 5 exhibits a ball of radius 10−2410^{-24}. The two-dimensional case, the pairs (∑1/n,∑1/(n+1))(\sum1/n,\sum1/(n+1)), is the older theorem of Erdős and Straus that the question of Erdős and Graham sought to extend; Kovač and Tao's later extension to every dimension has its own page.

The paper's digest is the library card Kovač 2024.

Read depth. The theorem is stated as in the arXiv v3 text; the published text was not compared line by line, and the proof is not compiled here, so this project has made no independent review of it.

Formalization. Two Lean 4 developments declare themselves formalizations of this paper's proof and are linked above. The first is the gist that the formal-conjectures statement file (FormalConjectures/ErdosProblems/268.lean) names in its formal_proof attribute, at the revision the attribute pins: its header names Matteo Del Vecchio and Aristotle (Harmonic) as authors, says that it follows Kovač's answer, and cites Kovač's paper; its theorem harmonicSubseriesSet_interior_nonempty states the three-dimensional set's nonempty interior, and its source uses native_decide in one arithmetic step. The second, in the repository Jayyhk/erdos-lean, at the linked revision, carries the same header and, as a thread comment of 26 May 2026 reports, no native_decide. The formal-conjectures declaration itself states the theorem for every dimension, citing Kovač and Tao, with a sorry body. Neither file contains sorry or an axiom command at the linked revision. This project has built neither file nor audited their statements against the problem, so no formalized evidence is listed; the site's label PROVED (LEAN) refers to these developments.

Acceptance. The paper is refereed: V. Kovač, On the set of points represented by harmonic subseries, Amer. Math. Monthly 132, no. 9 (2025), 895--911. The site's curator, Thomas F. Bloom, marks Problem 268 proved and credits this paper with the answer and the explicit open ball. The page is dated by the arXiv posting of 13 May 2024.