Conjectures.io

Number theory

Erdős 1094

For all n≥2kn\ge 2k the least prime factor of (nk)\binom{n}{k} is ≤max⁡(n/k,k)\le\max(n/k,k), with only finitely many exceptions.

References

No one has attempted this yet.

Formal statement

Lean type

{(n, k) | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite

What you must prove

import FormalConjectures.ErdosProblems.«1094»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1094.erdos_1094" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1094.lean

Source type SHA-256
sha256:304f28163171d637cbf5ea5eaab880fd08ac58fd8276425ec6321c3f316237d1
Task id
fc-379fc029-erdos1094-erdos-1094-1ec3e802ca-formalized-v1
Task commitment
sha256:7fec5442cdd172da66e20451041ae1d482a7333fbcc6484bbdcb3f86d7747c8c

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.