A published paper or arXiv preprint answers the main question of Erdős Problem #289 (theorem erdos_289 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

The problem, as stated in formal-conjectures (Apache 2.0):

Is it true that, for all sufficiently large k, there exist finite intervals I_1, \dotsc, I_k \subset \mathbb{N}, distinct, not overlapping or adjacent, with |I_i| \geq 2 for 1 \leq i \leq k such that 1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}? Here two intervals are adjacent if their union is again an interval, so any two of the I_i must be separated by at least one integer. This is true: a formal proof in Lean 4 was produced by the LEAP prover agent [Ku+26] (see the linked `formal_proof`). We note that other recent solutions were also posted ahead of this one (see [erdosproblems.com/forum/thread/289/proof-claims](https://www.erdosproblems.com/forum/thread/289/proof-claims)); this formalization follows an independent, different proof path.

References formal-conjectures lists for this problem (a starting point, not evidence):

• [Ku+26] Kung, P.-N., Song, L., Hwang, D., Yoon, J., Li, C.-L., Severini, S., Olšák, M., Lockhart, E., Le, Q. V., Gokturk, B., Luong, T., Pfister, T., & Peng, N. (2026). _LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks_. arXiv:2606.03303.