Erdős Problem 288

Stream: Formal conjectures

[Anirudh Rao]

Hey I'm formalizing Erdős Problem 288 and I was a bit confused by the wording of the last sentence, "It is perhaps true with two intervals replaced by any k intervals."

This is how I've formalized it now:

theorem erdos_288.variants.k_intervals : ∃ k, Set.Finite { I : Fin k → ℕ × ℕ |
      ∃ n : ℕ, (∑ j : Fin k, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n
    } ↔ answer(sorry) := by
  sorry

I'm not sure if $k$ is supposed to be an exist or forall quantifier... what do you all think?

[Yan Yablonovskiy 🇺🇦]

I guess I would be nervous about the case of k = 1, and (1,1). And perhaps also the casting between Rat and Nat.

[Anirudh Rao]

Oh, true! I didn't realize I was also assuming k > 2 but not stating it. Thanks for the catch!

[Anirudh Rao]

I think the casting works out fine. Or at the very least, I can't find mistakes

[Moritz Firsching]

Looking at the original source
[ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial number theory*. Monographies de L'Enseignement Mathematique (1980) perhaps the quantifiers become more clear (on page 34):

Suppose we let $\Sigma_{a,b}$ denote the sum $\sum_{i=0}^{b-a} \frac{1}{a+i}$. It is probably true that $\Sigma_{a,b} + \Sigma_{c,d}$ is an integer only finitely often. However this will probably be difficult to prove since we can not even show that $\Sigma_{a,b} + \frac{1}{n}$ is an integer only a finite number of times. Perhaps for each $k$, $\sum_{i=1}^k \Sigma_{a_i, b_i}$ can be an integer only finitely often. It seems likely that for large $k$, we can always write $1 = \sum_{i=1}^k \Sigma_{a_i, b_i}$ with $b_i > a_i$ (e.g., see [Hah (78)]). An example [Mon (79)] of such a representation for 2 is given by taking the denominators $\{ 2, 3, 4, 5, 6, 7, 9, 10, 17, 18, 34, 35, 84, 85 \}$. It is not hard to show that

[Anirudh Rao]

Thanks! :slight_smile: I couldn't find the original problem from the site, the site's linked pdf doesn't include all the pages that are here