Conjectures.io

Number theory

Erdős 727 - k 2

It is open even for k=2k = 2. Let k=2k = 2. Does ((n+k)!)2∣(2n)!((n+k)!)^2∣(2n)! hold for infinitely many n?

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ {n | (n + 2).factorial ^ 2 ∣ (2 * n).factorial}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«727»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos727.erdos_727.variants.k_2" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/727.lean

Source type SHA-256
sha256:fd6640da42952371709f4bac8d9c66cc89d0d511eb0ec40d86975eb97d39c34e
Task id
fc-379fc029-variants-k-2-e7bee98737-formalized-v1
Task commitment
sha256:dfa07456b949dc3b8dbacd193478452e5588fabc4784ee8548fe0da37ab1bdeb

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.