Erdős problem 729 · problems.science

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

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

1 retained statement2415f78e850a

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.

Sources

Search problems.science