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 of Problem 268, the triples
over infinite with , 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 , 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 . The two-dimensional case, the pairs , 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.