Erdős Problem 728

Theorem 728 · Erdős

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.

Formal statement · Lean 4.lean

theorem erdos_728 :
    answer(True) ↔
      ∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
        ∃ a b n : ℕ,
          0 < n ∧
          ε * n < a ∧
          ε * n < b ∧
          a ! * b ! ∣ n ! * (a + b - n)! ∧
          a + b > n + C * log n ∧
          a + b < n + C' * log n := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗