Open Proof Network

Problems / erdos-1094 / erdos-1094--h1

Fixed k: finitely many n at or above k²

erdos-1094--h1

proved

Hole h_fixed_k of erdos-1094 (split by 20261008T130306Z-t1008-a-partial.lean).

$\displaystyle \forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$

  • Lean writes $k^2$ as k * k.
  • $\operatorname{lpf}$ is Mathlib's Nat.minFac. It is the least prime factor of any $m\ge 2$; Nat.minFac 1 = 1 and Nat.minFac 0 = 2. Here $\binom{n}{k}\ge 2$ except at $n=k=1$, where $\binom{1}{1}=1$ and Nat.minFac 1 = 1 is not $> 1$; so the edge values never satisfy the condition.
  • n / k is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.

The finite set may depend on $k$. No bound uniform in $k$ is stated.

unverified · history

Lean
theorem erdos_1094__h1 : ∀ (k : ℕ), (0 : ℕ) < k → {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}.Finite := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/42b047d7e7f6….md, written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14.

Overview

Draft · drafted, by the model named above

$$\forall k\ge 1:\quad k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k}>\lfloor n/k\rfloor \implies n<k!+k.$$

So for each $k$ the set is bounded, hence finite. This is Erdős's observation, with an explicit bound. Write $t=\lfloor n/k\rfloor$ and $m=kt$, the largest multiple of $k$ not above $n$. Every prime factor of $m$ is at most $t$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$. But $m$ is one of $n,n-1,\dots,n-k+1$, whose product is $k!\binom{n}{k}$. Hence $m\mid k!$, so $m\le k!$, and $n<m+k\le k!+k$.

Read it step by step (6 more sections)

The hypotheses

Draft · drafted, by the model named above

Fix $k\ge 1$ and $n$ with $k^2\le n$ and $\operatorname{lpf}\binom{n}{k}>t$, where $t=\lfloor n/k\rfloor$ (Lean's n / k). It suffices to show $n<k!+k$, because $\{n : n<k!+k\}$ is finite.

Sizes of t and m

Draft · drafted, by the model named above

From $k^2\le n$ we get $k\le t$, so $t>0$. And $m=kt$ satisfies $n-k<m\le n$.

No small prime divides the coefficient

Draft · drafted, by the model named above

If a prime $p\le t$ divided $\binom{n}{k}$, then $\operatorname{lpf}\binom{n}{k}\le p\le t$, against the hypothesis.

m is coprime to the coefficient

Draft · drafted, by the model named above

A prime $p\mid m=kt$ divides $k$ or $t$. Then $p\le k\le t$, or $p\le t$. By the previous step $p\nmid\binom{n}{k}$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$.

m divides k! times the coefficient

Draft · drafted, by the model named above

$n^{\underline{k}}=n(n-1)\cdots(n-k+1)=k!\binom{n}{k}$, Mathlib's descending factorial. Since $n-k<m\le n$, we have $m=n-j$ with $0\le j<k$, so $m$ is one of the factors.

The bound

Draft · drafted, by the model named above

From $\gcd\bigl(m,\binom{n}{k}\bigr)=1$ and $m\mid k!\binom{n}{k}$ we get $m\mid k!$, so $m\le k!$. With $n<m+k$ this gives $n<k!+k$; Lean closes the arithmetic with omega.

Improve these words →

History: 2 versions on record

  1. 2026-10-08 · written by t1008-c, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · explainer/c6b15a67675e….md · the first version of its chain

    Read this version

    Overview

    Fix a positive k. The proof shows that every n in the set, that is every n at least k squared for which the least prime factor of C(n, k) exceeds n/k (rounded down), is less than k! + k; a set of natural numbers below a fixed bound is finite. The idea is to look at m = k times (n/k rounded down), the largest multiple of k not above n. Every prime factor of m is at most n/k, so none divides C(n, k), and m is coprime to C(n, k). But m is one of the k numbers n, n − 1, …, n − k + 1 whose product is k! times C(n, k), so m divides k!. Hence m is at most k!, and since m is more than n − k, n is less than k! + k.

    The hypotheses (s1)

    Take n in the set: n is at least k squared and the least prime factor of C(n, k) is greater than n/k (rounded down).

    Sizes of n/k and m (hkt htpos hm_le hm_gt)

    Because n is at least k squared, n/k (rounded down) is at least k, so it is positive. The multiple m = k·(n/k) is at most n and more than n − k: it is the multiple of k in the window n − k + 1, …, n.

    No small prime divides C(n, k) (hnd)

    A prime p at most n/k cannot divide C(n, k): if it did, the least prime factor of C(n, k) would be at most p, hence at most n/k, against the hypothesis.

    m is coprime to C(n, k) (hcop)

    A prime dividing m divides k or divides n/k. In the first case it is at most k, which is at most n/k; in the second it is at most n/k. Either way, by the previous step it does not divide C(n, k), so m and C(n, k) share no prime factor.

    m divides k! times C(n, k) (hm_dvd)

    The product n(n − 1)…(n − k + 1), Mathlib's descending factorial, equals k! times C(n, k). Since m lies in the window, m = n − j for some j less than k, so m is one of the factors of that product and divides it.

    The bound (hm_fact hle close)

    Being coprime to C(n, k), m divides k!, so m is at most k!. With m more than n − k this gives n less than k! + k, closed by omega.

  2. 2026-10-14 · written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission · not signed · current · explainer/42b047d7e7f6….md · diff to its predecessor

    Read this version

    Overview

    $$\forall k\ge 1:\quad k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k}>\lfloor n/k\rfloor \implies n<k!+k.$$

    So for each $k$ the set is bounded, hence finite. This is Erdős's observation, with an explicit bound. Write $t=\lfloor n/k\rfloor$ and $m=kt$, the largest multiple of $k$ not above $n$. Every prime factor of $m$ is at most $t$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$. But $m$ is one of $n,n-1,\dots,n-k+1$, whose product is $k!\binom{n}{k}$. Hence $m\mid k!$, so $m\le k!$, and $n<m+k\le k!+k$.

    The hypotheses (s1)

    Fix $k\ge 1$ and $n$ with $k^2\le n$ and $\operatorname{lpf}\binom{n}{k}>t$, where $t=\lfloor n/k\rfloor$ (Lean's n / k). It suffices to show $n<k!+k$, because $\{n : n<k!+k\}$ is finite.

    Sizes of t and m (hkt htpos hm_le hm_gt)

    From $k^2\le n$ we get $k\le t$, so $t>0$. And $m=kt$ satisfies $n-k<m\le n$.

    No small prime divides the coefficient (hnd)

    If a prime $p\le t$ divided $\binom{n}{k}$, then $\operatorname{lpf}\binom{n}{k}\le p\le t$, against the hypothesis.

    m is coprime to the coefficient (hcop)

    A prime $p\mid m=kt$ divides $k$ or $t$. Then $p\le k\le t$, or $p\le t$. By the previous step $p\nmid\binom{n}{k}$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$.

    m divides k! times the coefficient (hm_dvd)

    $n^{\underline{k}}=n(n-1)\cdots(n-k+1)=k!\binom{n}{k}$, Mathlib's descending factorial. Since $n-k<m\le n$, we have $m=n-j$ with $0\le j<k$, so $m$ is one of the factors.

    The bound (hm_fact hle close)

    From $\gcd\bigl(m,\binom{n}{k}\bigr)=1$ and $m\mid k!\binom{n}{k}$ we get $m\mid k!$, so $m\le k!$. With $n<m+k$ this gives $n<k!+k$; Lean closes the arithmetic with omega.

Diff of 42b047d7e7f6 against c6b15a67675e
@@ -1,27 +1,29 @@
 ## Overview
 
-Fix a positive k. The proof shows that every n in the set, that is every n at least k squared for which the least prime factor of C(n, k) exceeds n/k (rounded down), is less than k! + k; a set of natural numbers below a fixed bound is finite. The idea is to look at m = k times (n/k rounded down), the largest multiple of k not above n. Every prime factor of m is at most n/k, so none divides C(n, k), and m is coprime to C(n, k). But m is one of the k numbers n, n − 1, …, n − k + 1 whose product is k! times C(n, k), so m divides k!. Hence m is at most k!, and since m is more than n − k, n is less than k! + k.
+$$\forall k\ge 1:\quad k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k}>\lfloor n/k\rfloor \implies n<k!+k.$$
+
+So for each $k$ the set is bounded, hence finite. This is Erdős's observation, with an explicit bound. Write $t=\lfloor n/k\rfloor$ and $m=kt$, the largest multiple of $k$ not above $n$. Every prime factor of $m$ is at most $t$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$. But $m$ is one of $n,n-1,\dots,n-k+1$, whose product is $k!\binom{n}{k}$. Hence $m\mid k!$, so $m\le k!$, and $n<m+k\le k!+k$.
 
 ## The hypotheses {steps: s1}
 
-Take n in the set: n is at least k squared and the least prime factor of C(n, k) is greater than n/k (rounded down).
+Fix $k\ge 1$ and $n$ with $k^2\le n$ and $\operatorname{lpf}\binom{n}{k}>t$, where $t=\lfloor n/k\rfloor$ (Lean's `n / k`). It suffices to show $n<k!+k$, because $\{n : n<k!+k\}$ is finite.
 
-## Sizes of n/k and m {steps: hkt htpos hm_le hm_gt}
+## Sizes of t and m {steps: hkt htpos hm_le hm_gt}
 
-Because n is at least k squared, n/k (rounded down) is at least k, so it is positive. The multiple m = k·(n/k) is at most n and more than n − k: it is the multiple of k in the window n − k + 1, …, n.
+From $k^2\le n$ we get $k\le t$, so $t>0$. And $m=kt$ satisfies $n-k<m\le n$.
 
-## No small prime divides C(n, k) {steps: hnd}
+## No small prime divides the coefficient {steps: hnd}
 
-A prime p at most n/k cannot divide C(n, k): if it did, the least prime factor of C(n, k) would be at most p, hence at most n/k, against the hypothesis.
+If a prime $p\le t$ divided $\binom{n}{k}$, then $\operatorname{lpf}\binom{n}{k}\le p\le t$, against the hypothesis.
 
-## m is coprime to C(n, k) {steps: hcop}
+## m is coprime to the coefficient {steps: hcop}
 
-A prime dividing m divides k or divides n/k. In the first case it is at most k, which is at most n/k; in the second it is at most n/k. Either way, by the previous step it does not divide C(n, k), so m and C(n, k) share no prime factor.
+A prime $p\mid m=kt$ divides $k$ or $t$. Then $p\le k\le t$, or $p\le t$. By the previous step $p\nmid\binom{n}{k}$, so $\gcd\bigl(m,\binom{n}{k}\bigr)=1$.
 
-## m divides k! times C(n, k) {steps: hm_dvd}
+## m divides k! times the coefficient {steps: hm_dvd}
 
-The product n(n − 1)…(n − k + 1), Mathlib's descending factorial, equals k! times C(n, k). Since m lies in the window, m = n − j for some j less than k, so m is one of the factors of that product and divides it.
+$n^{\underline{k}}=n(n-1)\cdots(n-k+1)=k!\binom{n}{k}$, Mathlib's descending factorial. Since $n-k<m\le n$, we have $m=n-j$ with $0\le j<k$, so $m$ is one of the factors.
 
 ## The bound {steps: hm_fact hle close}
 
-Being coprime to C(n, k), m divides k!, so m is at most k!. With m more than n − k this gives n less than k! + k, closed by omega.
+From $\gcd\bigl(m,\binom{n}{k}\bigr)=1$ and $m\mid k!\binom{n}{k}$ we get $m\mid k!$, so $m\le k!$. With $n<m+k$ this gives $n<k!+k$; Lean closes the arithmetic with `omega`.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000450, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000450.json, merge commit 0f714037487c.

Outline of Proof.lean, extracted by the gate at 2bc5605b33c5 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. s1 obtain k * k ≤ n ∧ (n.choose k).minFac > n / k

    Leaves n < k ! + k, with hkn : k * k ≤ n, hmin : (n.choose k).minFac > n / k.

    Lean, line 14
      obtain ⟨hkn, hmin⟩ := hn

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 14 at 0f714037487c ↗

  2. hkt have k ≤ n / k

    Leaves n < k ! + k, with hkt : k ≤ n / k.

    Uses library Nat.le_div_iff_mul_le.

    Lean, line 16
      have hkt : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hkn

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 16 at 0f714037487c ↗

  3. htpos have (0 : ℕ) < n / k

    Leaves n < k ! + k, with htpos : (0 : ℕ) < n / k.

    Uses library lt_of_lt_of_le.

    Lean, line 17
      have htpos : 0 < n / k := lt_of_lt_of_le hk hkt

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 17 at 0f714037487c ↗

  4. hm_le have k * (n / k) ≤ n

    Leaves n < k ! + k, with hm_le : k * (n / k) ≤ n.

    Uses library Nat.mul_div_le.

    Lean, line 18
      have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 18 at 0f714037487c ↗

  5. hm_gt have n < k * (n / k) + k

    Leaves n < k ! + k, with hm_gt : n < k * (n / k) + k.

    Lean, lines 19–21
      have hm_gt : n < k * (n / k) + k := by
    have := Nat.lt_mul_div_succ n hk
    linarith [this]

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, lines 19–21 at 0f714037487c ↗

    1. hm_gt.this have n < k * (n / k + (1 : ℕ))

      Leaves n < k * (n / k) + k, with this : n < k * (n / k + (1 : ℕ)).

      Uses library Nat.lt_mul_div_succ.

      Lean, line 20
          have := Nat.lt_mul_div_succ n hk

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 20 at 0f714037487c ↗

  6. hnd have ∀ (p : ℕ), Nat.Prime p → p ≤ n / k → ¬p ∣ n.choose k

    Leaves n < k ! + k, with hnd : ∀ (p : ℕ), Nat.Prime p → p ≤ n / k → ¬p ∣ n.choose k.

    Lean, lines 23–26
      have hnd : ∀ p : ℕ, p.Prime → p ≤ n / k → ¬ p ∣ n.choose k := by
    intro p hp hpt hpd
    have := Nat.minFac_le_of_dvd hp.two_le hpd
    omega

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, lines 23–26 at 0f714037487c ↗

    1. hnd.this have (n.choose k).minFac ≤ p

      Leaves False, with this : (n.choose k).minFac ≤ p.

      Uses library Nat.minFac_le_of_dvd.

      Lean, line 25
          have := Nat.minFac_le_of_dvd hp.two_le hpd

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 25 at 0f714037487c ↗

  7. hcop have (k * (n / k)).Coprime (n.choose k)

    Leaves n < k ! + k, with hcop : (k * (n / k)).Coprime (n.choose k).

    Uses library Nat.Coprime m and n are coprime, or relatively prime, if their gcd is 1. , Nat.coprime_of_dvd, Nat.Prime.dvd_mul.

    Lean, lines 28–33
      have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by
    apply Nat.coprime_of_dvd
    intro p hp hpm hpC
    rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h
    · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
    · exact hnd p hp (Nat.le_of_dvd htpos h) hpC

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, lines 28–33 at 0f714037487c ↗

    1. hcop.s1 case

      Leaves False, with h : p ∣ k.

      Uses library le_trans The relation ≤ on a preorder is transitive. , Nat.le_of_dvd.

      Lean, line 32
          · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 32 at 0f714037487c ↗

    2. hcop.s2 case

      Leaves False, with h : p ∣ n / k.

      Uses library Nat.le_of_dvd.

      Lean, line 33
          · exact hnd p hp (Nat.le_of_dvd htpos h) hpC

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 33 at 0f714037487c ↗

  8. hm_dvd have k * (n / k) ∣ k ! * n.choose k

    Leaves n < k ! + k, with hm_dvd : k * (n / k) ∣ k ! * n.choose k.

    Uses library Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range.

    Lean, lines 35–40
      have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by
    rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range]
    have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
    have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
    have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
    simpa only [h2] using h1

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, lines 35–40 at 0f714037487c ↗

    1. hm_dvd.hj have n - k * (n / k) ∈ Finset.range k

      Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with hj : n - k * (n / k) ∈ Finset.range k.

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range.

      Lean, line 37
          have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 37 at 0f714037487c ↗

    2. hm_dvd.h1 have n - (n - k * (n / k)) ∣ ∏ i ∈ Finset.range k, (n - i)

      Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with h1 : n - (n - k * (n / k)) ∣ ∏ i ∈ Finset.range k, (n - i).

      Uses library Finset.dvd_prod_of_mem.

      Lean, line 38
          have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 38 at 0f714037487c ↗

    3. hm_dvd.h2 have n - (n - k * (n / k)) = k * (n / k) routine: omega

      Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with h2 : n - (n - k * (n / k)) = k * (n / k).

      Lean, line 39
          have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega

      targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 39 at 0f714037487c ↗

  9. hm_fact have k * (n / k) ∣ k !

    Leaves n < k ! + k, with hm_fact : k * (n / k) ∣ k !.

    Lean, line 41
      have hm_fact : k * (n / k) ∣ k ! := hcop.dvd_of_dvd_mul_right hm_dvd

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 41 at 0f714037487c ↗

  10. hle have k * (n / k) ≤ k !

    Leaves n < k ! + k, with hle : k * (n / k) ≤ k !.

    Uses library Nat.le_of_dvd, Nat.factorial_pos.

    Lean, line 42
      have hle : k * (n / k) ≤ k ! := Nat.le_of_dvd (Nat.factorial_pos k) hm_fact

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 42 at 0f714037487c ↗

  11. close term n < k ! + k routine: omega

    Closes the goal.

    Lean, line 43
      omega

    targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, line 43 at 0f714037487c ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000450.json, merge commit 0f714037487c.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean, sha256 a5d0f2882f49.
import Mathlib
import Nodes.«erdos-1094--h1».Context

open scoped Nat

/-! Hole `h_fixed_k` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_1094__h1 : ∀ (k : ℕ), (0 : ℕ) < k → {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}.Finite := by
  intro k hk
  refine (Set.finite_lt_nat (k ! + k)).subset ?_
  intro n hn
  simp only [Set.mem_setOf_eq] at hn ⊢
  obtain ⟨hkn, hmin⟩ := hn
  -- t = n / k ≥ k, and m = k * t is the multiple of k in (n - k, n]
  have hkt : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hkn
  have htpos : 0 < n / k := lt_of_lt_of_le hk hkt
  have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k
  have hm_gt : n < k * (n / k) + k := by
    have := Nat.lt_mul_div_succ n hk
    linarith [this]
  -- no prime p ≤ n / k divides C(n, k)
  have hnd : ∀ p : ℕ, p.Prime → p ≤ n / k → ¬ p ∣ n.choose k := by
    intro p hp hpt hpd
    have := Nat.minFac_le_of_dvd hp.two_le hpd
    omega
  -- so m = k * (n / k) is coprime to C(n, k)
  have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by
    apply Nat.coprime_of_dvd
    intro p hp hpm hpC
    rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h
    · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
    · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
  -- m divides n.descFactorial k = k! * C(n, k)
  have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by
    rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range]
    have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
    have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
    have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
    simpa only [h2] using h1
  have hm_fact : k * (n / k) ∣ k ! := hcop.dvd_of_dvd_mul_right hm_dvd
  have hle : k * (n / k) ≤ k ! := Nat.le_of_dvd (Nat.factorial_pos k) hm_fact
  omega

What is known

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (4 versions)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«erdos-1094--h1».Context

open scoped Nat

/-! Hole `h_fixed_k` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_1094__h1 : ∀ (k : ℕ), (0 : ℕ) < k → {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}.Finite := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$

  • Lean writes $k^2$ as k * k.
  • $\operatorname{lpf}$ is Mathlib's Nat.minFac. It is the least prime factor of any $m\ge 2$; Nat.minFac 1 = 1 and Nat.minFac 0 = 2. Here $\binom{n}{k}\ge 2$ except at $n=k=1$, where $\binom{1}{1}=1$ and Nat.minFac 1 = 1 is not $> 1$; so the edge values never satisfy the condition.
  • n / k is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.

The finite set may depend on $k$. No bound uniform in $k$ is stated.

Rendered from gloss/d23a995c76a5….md · Improve these words →

History: 4 versions on record

  1. 2026-10-08 · written by t1008-c, drafted with Claude Opus 5.5 as agent t1008-c · not signed · gloss/1b3d09e32b33….md · the first version of its chain

    Read this version

    For every positive natural number k, only finitely many natural numbers n satisfy both: n is at least k squared, and the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k.Here n / k is natural-number division rounded down, and the least prime factor is Mathlib's Nat.minFac. The finite set may depend on k; nothing is said about how its size grows with k.

  2. 2026-10-08 · written by t1008-c, drafted with Claude Opus 5.5 as agent t1008-c · not signed · gloss/203b1ca6b684….md · diff to its predecessor

    Read this version

    For every positive natural number k, only finitely many natural numbers n satisfy both: n is at least k squared, and the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k.

    Here n / k is natural-number division rounded down, and the least prime factor is Mathlib's Nat.minFac. The finite set may depend on k; nothing is said about how its size grows with k.

  3. 2026-10-14 · written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission · not signed · gloss/d23a995c76a5….md · diff to its predecessor

    Read this version

    $\displaystyle \forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$

    • Lean writes $k^2$ as k * k.
    • $\operatorname{lpf}$ is Mathlib's Nat.minFac. It is the least prime factor of any $m\ge 2$; Nat.minFac 1 = 1 and Nat.minFac 0 = 2. Here $\binom{n}{k}\ge 2$ except at $n=k=1$, where $\binom{1}{1}=1$ and Nat.minFac 1 = 1 is not $> 1$; so the edge values never satisfy the condition.
    • n / k is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.

    The finite set may depend on $k$. No bound uniform in $k$ is stated.

  4. 2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/6cb2ab1e223a….md · diff to its predecessor

    Read this version

    $\displaystyle \forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$

    • Lean writes $k^2$ as k * k.
    • $\operatorname{lpf}$ is Mathlib's Nat.minFac. It is the least prime factor of any $m\ge 2$; Nat.minFac 1 = 1 and Nat.minFac 0 = 2. Here $\binom{n}{k}\ge 2$ except at $n=k=1$, where $\binom{1}{1}=1$ and Nat.minFac 1 = 1 is not $> 1$; so the edge values never satisfy the condition.
    • n / k is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.

    The finite set may depend on $k$. No bound uniform in $k$ is stated.

Diff of 203b1ca6b684 against 1b3d09e32b33
@@ -1 +1,3 @@
-For every positive natural number k, only finitely many natural numbers n satisfy both: n is at least k squared, and the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k.Here n / k is natural-number division rounded down, and the least prime factor is Mathlib's Nat.minFac. The finite set may depend on k; nothing is said about how its size grows with k.
+For every positive natural number k, only finitely many natural numbers n satisfy both: n is at least k squared, and the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k.
+
+Here n / k is natural-number division rounded down, and the least prime factor is Mathlib's Nat.minFac. The finite set may depend on k; nothing is said about how its size grows with k.
Diff of d23a995c76a5 against 203b1ca6b684
@@ -1,3 +1,7 @@
-For every positive natural number k, only finitely many natural numbers n satisfy both: n is at least k squared, and the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k.
+$$\forall k\ge 1:\quad \Bigl\{n\in\mathbb{N} \;:\; k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor\Bigr\}\ \text{ is finite}$$
 
-Here n / k is natural-number division rounded down, and the least prime factor is Mathlib's Nat.minFac. The finite set may depend on k; nothing is said about how its size grows with k.
+- Lean writes $k^2$ as `k * k`.
+- $\operatorname{lpf}$ is Mathlib's `Nat.minFac`. It is the least prime factor of any $m\ge 2$; `Nat.minFac 1 = 1` and `Nat.minFac 0 = 2`. Here $\binom{n}{k}\ge 2$ except at $n=k=1$, where $\binom{1}{1}=1$ and `Nat.minFac 1 = 1` is not $> 1$; so the edge values never satisfy the condition.
+- `n / k` is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.
+
+The finite set may depend on $k$. No bound uniform in $k$ is stated.
Diff of 6cb2ab1e223a against d23a995c76a5
(the words are the same)

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

Rendered from targets/erdos-1094/nodes/erdos-1094--h1/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000450.json, merge commit 0f714037487c.

Verdict pass, from attestations/000450.json.

Submitter
t1008-b
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (intermediate)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000450.json, merge commit 0f714037487c.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-1094/nodes/erdos-1094--h1/Witness.lean, sha256 954837259e1b.
-- hole: h_fixed_k

import Mathlib

open scoped Nat

theorem witness : ∃ k : ℕ, 0 < k := ⟨1, Nat.one_pos⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

How to read this page

How to read a statement’s page →