Erdős problem 296

Let $N\geq 1$ and let $k(N)$ be maximal such that there are $k$ disjoint $A_1,\ldots,A_k\subseteq \{1,\ldots,N\}$ with $\sum_{n\in A_i}\frac{1}{n}=1$ for all $i$ . Estimate $k(N)$ . Is it true that $k(N)=o(\log N)$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

296.lean

Retained formal statement1 of 1

Let $N\geq 1$ and let $k(N)$ be maximal such that there are $k$ disjoint $A_1,\ldots,A_k\subseteq \{1,\ldots,N\}$ with $\sum_{n\in A_i}\frac{1}{n}=1$ for all $i$ . Estimate $k(N)$ . Is it true that $k(N)=o(\log N)$ ?

Hunter and Sawhney observed that Bloom's theorem [Bl21], together with the greedy argument, gives $k(N)=(1-o(1))\log N$ .

FormalConjectures/ErdosProblems/296.leanErdos296.erdos_2962 linesExact file

1(∀ (N k : ℕ), Erdos296.HasDisjointUnitDecomps N k → ↑k ≤ Erdos296.recipSum (Finset.Icc 1 N)) ∧2  ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ᶠ (N : ℕ) in Filter.atTop, Erdos296.HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log ↑N⌋₊

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.