Erdős Problem #728

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.