Erdős problem 729

Let $C>0$ be a constant. Are there infinitely many integers $a,b,n$ with $a+b> n+C\log n$ such that the denominator of $\frac{n!}{a!b!}$ contains only primes $\ll_C 1$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

729.lean

Retained formal statement1 of 1

Let $C>0$ be a constant. Are there infinitely many integers $a,b,n$ with $a+b> n+C\log n$ such that the denominator of $\frac{n!}{a!b!}$ contains only primes $\ll_C 1$ ?

Erdős [Er68c] proved that if $a!b!\mid n!$ then $a+b\leq n+O(\log n)$ . This has been proved in the affirmative by Barreto and Leeham, using ChatGPT and Aristotle, with a modification of the argument used for [728].

FormalConjectures/ErdosProblems/729.leanErdos729.erdos_72910 linesExact file

1True ↔2  ∀ C > 0,3    ∃ K ≥ 3,4      {(a, b, n) |5          a > 0 ∧6            b > 0 ∧7              n > 0 ∧8                ↑a + ↑b > ↑n + C * Real.log ↑n ∧9                  ∀ (p : ℕ),10                    Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite

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.