Erdős problem 728 · problems.science

Whether there are infinitely many integers $a, b, n$ with $a, b \ge \varepsilon n$ such that $a!\cdot b!$ divides $n!\cdot(a+b-n)!$ while $a+b$ exceeds $n$ by more than $C\cdot\log n$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

728.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/728.leanErdos728.erdos_72810 linesExact file

1True ↔2  ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0),3    ∀ C > 0,4      ∀ C' > C,5        ∃ a b n,6          0 < n ∧7            ε * ↑n < ↑a ∧8              ε * ↑n < ↑b ∧9                a.factorial * b.factorial ∣ n.factorial * (a + b - n).factorial ∧10                  ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ↑a + ↑b < ↑n + C' * 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.

Sources

Search problems.science