Number theory · Last catalog review 26 Jul 2026

Erdős Problem 1094

For all

n\ge 2k

the least prime factor of

\binom{n}{k}

\le\max(n/k,k)

, with only finitely many exceptions.

References

erdosproblems.com/1094

Published 1 Aug 2026Never attempted

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-e923379e-erdos1094-erdos-1094-e88b987211-formalized-v1
Task commitment: sha256:c70c6d5ce5257f1071ab3a762e36a5a5f5baffb52e8676f00632ebe4cf6b4a48

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.