Erdős problem 727
Let . Does hold for infinitely many ?
Sources
FormalConjectures/ErdosProblems/
727.lean
Retained formal statement
Balakran proved this holds for .
Let . Does for infinitely many ?
True ↔ {n | (n + 1).factorial ^ 2 ∣ (2 * n).factorial}.InfiniteSolvedStatement only, no proof