Erdős Problem 728

Reference: erdosproblems.com/728

theorem Erdos728.erdos_728 : True ↔ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ C > 0, ∀ C' > C, ∃ (a : ℕ) (b : ℕ) (n : ℕ), 0 < n ∧ ε * ↑n < ↑a ∧ ε * ↑n < ↑b ∧ a.factorial * b.factorial ∣ n.factorial * (a + b - n).factorial ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ↑a + ↑b < ↑n + C' * Real.log ↑n

Let $\varepsilon$ be sufficiently small and $C, C' > 0$. Are there integers $a, b, n$ such that $$a, b > \varepsilon n\quad a!\, b! \mid n!\, (a + b - n)!, $$ and $$C \log n < a + b - n < C' \log n ?$$

Note that the website currently displays a simpler (trivial) version of this problem because $a + b$ isn't assumed to be in the $n + O(\log n)$ regime.

Barreto and ChatGPT-5.2 have proved that, for any $0 < C_1 < C_2$, there are infinitely many $a, b, n$ with $b = n/2$, $a = n/2 + O(\log n)$, and $C_1 \log n < a + b - n < C_2 \log n$ such that $a! b! \mid n! (a + b - n)!$

This appears to answer the question in the spirit it was intended.

This was formalized in Lean by Alexeev using Aristotle.