Open Proof Network

Problems / erdos-1094

erdos-1094

open Listed, and its statements accept work. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 1 candidate, 1 cluster, 8 questions waiting

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

Erdős problem 1094: For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/1094

ProvedExplainedWritten up

This problem is open for work. How to contribute →

Statements

65 statements. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.

proved A proof passed all nine checks and was merged. Proved is not the same as explained. protocol: proved open No proof has closed this statement and nothing blocks starting on it. Anyone may work on it now. protocol: ready · on the frontier blocked Waits on other statements, or on a definition that has not been checked yet. Not accepting work. A statement waiting only for its witness is not blocked in this sense: it needs a witness. protocol: blocked needs a witness Left open by a proof skeleton and waiting only for its witness. Supplying one is the work here and anyone may do it; once it merges, the statement is open for proof. protocol: blocked · cause witness-missing · on the frontier route: all of its holes A dot on the way down from a statement to the holes of one merged decomposition of it: the route closes the statement only when every hole beneath the dot is proved (AND). protocol: decompositions[] (D-12), routes (D-25 v3.40) any one route closes it A diamond under a statement that two or more routes, or a resolving variant, could close: any one of them suffices (OR), and so would a direct proof. protocol: routes (D-25 v3.40) depends on A solid line runs up from a statement to one that declared it as a dependency: the upper statement's proof may build on the lower one. protocol: deps (META.yaml) lemma from another branch A dash-dot line runs up from a statement under another branch to one whose merged decomposition restated it as a hole. The upper statement may draw on it once it is proved and never waits on it: a hole's standing, without a hole's place in the tree. protocol: lemmas (META.yaml, D-12 v3.38) has an outline A numbered tab: how many outlines the statement carries, an outline being an annex that names its steps. Its panel lists each one, which merged skeleton followed it and the statements that skeleton made, or that none has; an annex with no steps is listed under Notes and not counted. An outline is the contributor's own text, unverified. protocol: annex/v2 steps (D-31 v3.26) open, proposed Literature: Open problem: no proof is known — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45). known, proposed Literature: Known: a proof is published and not formalised — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45).
Ways to settle the problem A way to settle the problem: a sufficient set is a set of statements whose proofs would settle the problem's own statement, either proving it or refuting it through a variant whose relation the gate checked, with the closing proofs of the decomposed statements on the way still to submit: one choice of route at every fork. Each set says which way it settles the problem. The tree under this heading is the navigation device: select a set, a family of sets or one route choice and the drawing shows just that part. protocol: sufficient sets (D-25 v3.40, v3.46; F27)

Each set proves the problem or refutes it. Select a node or an edge to filter the drawing to that part of the proof; select it again to come back.

Small range 2k ≤ n < k²: k is bounded: 4 sets choose a route here — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. This is the one literature input the h_lo range needs. Small range 2k ≤ n < k²: k is bounded: 4 sets choose a route here — via Baker, Harman and Pintz (2001): for large k the interval (k, k + k^(21/40)) holds at least C k^(21/40) / log k primes. Stated exactly as `axiom bhp` in van Doorn and Tang's formalisation (github.com/Woett/ChatGPT-s-note-on-Erdos451), with `primeCard` unfolded. Residue form, k even: 2 sets choose a route here — via Small range through a last-digit carry: for large k some prime p ≤ k has n mod p < k mod p, so p divides C(n,k) by Lucas' theorem. Set 3 (proves): 6 open statements of 8 — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. The same hole closes erdos-1094--h2--h1. Set 4 (proves): 12 open statements of 14 — via Skeleton of Granville–Ramaré, Mathematika 43 (1996) 73–107, Theorem 8 (preprint p. 5), proof in §5e (preprint pp. 24–25). Their n is our n − k (they write C(n+k, k)). h_els: the input GR cite and do not prove (§5e, p. 24: "That n ≫ k²/log k has been proved in [ELS], so we may assume this"): Erdős–L… Set 1 (proves): 15 open statements of 17 — via Residue form with k even, split at the prime 3: either 3 | k, or 3 ∤ k and no carry at 3 (a carry at 3 is closed by p = 3). Set 2 (proves): 12 open statements of 14 — via Residue form with k even, split by whether some prime q ≤ k divides n but not k: such a q carries at once, so the hole is the case where every prime ≤ k dividing n divides k. Residue form, k even: 2 sets choose a route here — via Small range through a last-digit carry: for large k some prime p ≤ k has n mod p < k mod p, so p divides C(n,k) by Lucas' theorem. Set 7 (proves): 8 open statements of 10 — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. The same hole closes erdos-1094--h2--h1. Set 8 (proves): 10 open statements of 12 — via Skeleton of Granville–Ramaré, Mathematika 43 (1996) 73–107, Theorem 8 (preprint p. 5), proof in §5e (preprint pp. 24–25). Their n is our n − k (they write C(n+k, k)). h_els: the input GR cite and do not prove (§5e, p. 24: "That n ≫ k²/log k has been proved in [ELS], so we may assume this"): Erdős–L… Set 5 (proves): 13 open statements of 15 — via Residue form with k even, split at the prime 3: either 3 | k, or 3 ∤ k and no carry at 3 (a carry at 3 is closed by p = 3). Set 6 (proves): 10 open statements of 12 — via Residue form with k even, split by whether some prime q ≤ k divides n but not k: such a q carries at once, so the hole is the case where every prime ≤ k dividing n divides k. bounded k on k² ≤ n < k³: 8 sets choose a route here Set 1 (proves): 15 open statements of 17 — via Residue form with k even, split at the prime 3: either 3 | k, or 3 ∤ k and no carry at 3 (a carry at 3 is closed by p = 3). 1 Set 2 (proves): 12 open statements of 14 — via Residue form with k even, split by whether some prime q ≤ k divides n but not k: such a q carries at once, so the hole is the case where every prime ≤ k dividing n divides k. 2 Residue form, k even: 2 sets choose a route here — via Small range through a last-digit carry: for large k some prime p ≤ k has n mod p < k mod p, so p divides C(n,k) by Lucas' theorem. Set 3 (proves): 6 open statements of 8 — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. The same hole closes erdos-1094--h2--h1. 3 Set 4 (proves): 12 open statements of 14 — via Skeleton of Granville–Ramaré, Mathematika 43 (1996) 73–107, Theorem 8 (preprint p. 5), proof in §5e (preprint pp. 24–25). Their n is our n − k (they write C(n+k, k)). h_els: the input GR cite and do not prove (§5e, p. 24: "That n ≫ k²/log k has been proved in [ELS], so we may assume this"): Erdős–L… 4 Small range 2k ≤ n < k²: k is bounded: 4 sets choose a route here — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. This is the one literature input the h_lo range needs. Set 5 (proves): 13 open statements of 15 — via Residue form with k even, split at the prime 3: either 3 | k, or 3 ∤ k and no carry at 3 (a carry at 3 is closed by p = 3). 5 Set 6 (proves): 10 open statements of 12 — via Residue form with k even, split by whether some prime q ≤ k divides n but not k: such a q carries at once, so the hole is the case where every prime ≤ k dividing n divides k. 6 Residue form, k even: 2 sets choose a route here — via Small range through a last-digit carry: for large k some prime p ≤ k has n mod p < k mod p, so p divides C(n,k) by Lucas' theorem. Set 7 (proves): 8 open statements of 10 — via Konyagin's theorem, g(k) > k^3 for all large k, in the network's "bounded k" shape: a binomial coefficient C(n, k) with 2k ≤ n < k^3 whose prime factors all exceed k occurs only for bounded k. The same hole closes erdos-1094--h2--h1. 7 Set 8 (proves): 10 open statements of 12 — via Skeleton of Granville–Ramaré, Mathematika 43 (1996) 73–107, Theorem 8 (preprint p. 5), proof in §5e (preprint pp. 24–25). Their n is our n − k (they write C(n+k, k)). h_els: the input GR cite and do not prove (§5e, p. 24: "That n ≫ k²/log k has been proved in [ELS], so we may assume this"): Erdős–L… 8 Small range 2k ≤ n < k²: k is bounded: 4 sets choose a route here — via Baker, Harman and Pintz (2001): for large k the interval (k, k + k^(21/40)) holds at least C k^(21/40) / log k primes. Stated exactly as `axiom bhp` in van Doorn and Tang's formalisation (github.com/Woett/ChatGPT-s-note-on-Erdos451), with `primeCard` unfolded. bounded k on k² ≤ n < k³: 8 sets choose a route here Erdős problem 1094: the problem's own statement
erdos-1094 (Erdős problem 1094): ready Erdős problem 1094 1 erdos-1094--h1 (Fixed k: finitely many n at or above k²): proved Fixed k: finitely many n at or above k² erdos-1094--h2 (bounded k on n ≥ k²): ready bounded k on n ≥ k² 1 Literature: open (proposed by t1009-b, awaits confirmation) erdos-1094--h2--h1 (bounded k on k² ≤ n < k³): ready bounded k on k² ≤ n < k³ 2 Literature: known (proposed by t1009-b, awaits confirmation) erdos-1094--h2--h1--h1 (C(n,k) with no prime factor ≤ k, 2k ≤ n < k³): ready C(n,k) with no prime factor ≤ k, 2k ≤ n < k³ Literature: known (proposed by t1009-c, awaits confirmation) erdos-1094--h2--h1--h1--h1 (2k ≤ n < k³ with n/gcd(n,k) free of primes ≤ k): ready 2k ≤ n < k³ with n/gcd(n,k) free of primes ≤ k erdos-1094--h2--h1--h1--h1--h1 (2k ≤ n < k² with n/gcd(n,k) free of primes ≤ k): ready 2k ≤ n < k² with n/gcd(n,k) free of primes ≤ k erdos-1094--h2--h1--h1--h1--h1--h1 (n prime in [2k, k^2)): ready n prime in [2k, k^2) erdos-1094--h2--h1--h1--h1--h1--h2 (n = g q with 2 <= g | k and q > k prime): ready n = g q with 2 <= g | k and q > k prime erdos-1094--h2--h1--h1--h1--h2 (k² ≤ n < k³ with n/gcd(n,k) free of primes ≤ k): ready k² ≤ n < k³ with n/gcd(n,k) free of primes ≤ k erdos-1094--h2--h1--h1--h1--h2--h1 (n = gcd(n,k) times one prime q > k): ready n = gcd(n,k) times one prime q > k erdos-1094--h2--h1--h1--h1--h2--h2 (n = gcd(n,k) times p q, two primes > k): ready n = gcd(n,k) times p q, two primes > k erdos-1094--h2--h1--h4 (the thin strip above k²): ready the thin strip above k² Literature: known (proposed by t1014-z, awaits confirmation) erdos-1094--h2--h1--h4--h1 (the thin strip with n/gcd(n,k) prime): ready the thin strip with n/gcd(n,k) prime erdos-1094--h2--h1--h4--h1--h1 (the thin strip with n prime and coprime to k): ready the thin strip with n prime and coprime to k erdos-1094--h2--h1--h4--h1--h2 (the thin strip with n/gcd(n,k) prime, gcd(n,k) ≥ 2): ready the thin strip with n/gcd(n,k) prime, gcd(n,k) ≥ 2 erdos-1094--h2--h1--h4--h1--h2--h1 (proper common divisor case): ready proper common divisor case erdos-1094--h2--h2 (bounded k on n ≥ k³): ready bounded k on n ≥ k³ 1 erdos-1094--h2--h2--h1 (BHP short-interval primes): ready BHP short-interval primes Literature: known (proposed by t1014-z, awaits confirmation) erdos-1094--h2--h2--h2 (van Doorn–Tang's theorem, unless BHP fails): proved van Doorn–Tang's theorem, unless BHP fails 1 Literature: known (proposed by t1014-x, awaits confirmation) erdos-1094--h2--h2--h2--h1 (small range 2k < n ≤ k^(2−21/40)/2): proved small range 2k < n ≤ k^(2−21/40)/2 erdos-1094--h2--h2--h2--h2 (medium range k^(2−21/40)/2 < n ≤ k²/log²k): proved medium range k^(2−21/40)/2 < n ≤ k²/log²k erdos-1094--h2--h2--h2--h2--h1 (medium range: few m with n/m near an integer): proved medium range: few m with n/m near an integer erdos-1094--h2--h2--h2--h3 (medium-large range k²/log²k < n ≤ k^(2+21/40)/2): proved medium-large range k²/log²k < n ≤ k^(2+21/40)/2 erdos-1094--h2--h2--h2--h3--h1 (Konyagin's bound on m with n/m near an integer): proved Konyagin's bound on m with n/m near an integer erdos-1094--h2--h2--h2--h3--h1--h1 (Konyagin's theorem: points where f is near a rational): proved Konyagin's theorem: points where f is near a rational erdos-1094--h2--h2--h2--h3--h1--h1--h1 (Konyagin's theorem at scale in [1, 2) when 65536X < 1): proved Konyagin's theorem at scale in [1, 2) when 65536X < 1 erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1 (a small integer linear relation on 2r points): proved a small integer linear relation on 2r points erdos-1094--h2--h2--h2--h4 (large range up to exp(log²k/(20 log log k))): proved large range up to exp(log²k/(20 log log k)) erdos-1094--h2--h2--h3 (beyond van Doorn–Tang's range, n ≥ k³): ready beyond van Doorn–Tang's range, n ≥ k³ erdos-1094--h2--h2--h3--h1 (beyond van Doorn–Tang with n/gcd(n,k) prime): ready beyond van Doorn–Tang with n/gcd(n,k) prime erdos-1094--h2--h2--h3--h1--h1 (beyond van Doorn–Tang, n/gcd(n,k) prime, k ∤ n): ready beyond van Doorn–Tang, n/gcd(n,k) prime, k ∤ n erdos-1094--h3 (Small range 2k ≤ n < k²: k is bounded): ready Small range 2k ≤ n < k²: k is bounded 1 Literature: known (proposed by t1009-a, awaits confirmation) erdos-1094--h3--h1 (Residue form: a prime p ≤ k with n mod p < k mod p): ready Residue form: a prime p ≤ k with n mod p < k mod p 1 erdos-1094--h3--h1--h1 (Residue form, k even): ready Residue form, k even erdos-1094--h3--h1--h1--h1 (Residue form, k even, 3 | k): ready Residue form, k even, 3 | k erdos-1094--h3--h1--h1--h1--h1 (Residue form, k even, 15 | k): ready Residue form, k even, 15 | k erdos-1094--h3--h1--h1--h1--h2 (Residue form, 6 | k, 5 ∤ k, no carry at 5): ready Residue form, 6 | k, 5 ∤ k, no carry at 5 erdos-1094--h3--h1--h1--h2 (Residue form, k even, 3 ∤ k, no carry at 3): ready Residue form, k even, 3 ∤ k, no carry at 3 erdos-1094--h3--h1--h1--h2--h1 (Residue form, k even, 3 ∤ k, no carry at 3 to 13): ready Residue form, k even, 3 ∤ k, no carry at 3 to 13 erdos-1094--h3--h1--h1--h2--h1--h1 (Residue form, k even, k ≡ 1 (mod 3), no carry at 3 to 13): ready Residue form, k even, k ≡ 1 (mod 3), no carry at 3 to 13 erdos-1094--h3--h1--h1--h2--h1--h2 (Residue form, k even, k ≡ n ≡ 2 (mod 3), no carry 5 to 13): ready Residue form, k even, k ≡ n ≡ 2 (mod 3), no carry 5 to 13 erdos-1094--h3--h1--h1--h3 (Residue form, k even, every prime ≤ k dividing n divides k): ready Residue form, k even, every prime ≤ k dividing n divides k erdos-1094--h3--h1--h2 (Residue form, k and n odd): ready Residue form, k and n odd erdos-1094--h3--h1--h2--h1 (Residue form, k and n odd, 3 | k): ready Residue form, k and n odd, 3 | k erdos-1094--h3--h1--h2--h1--h1 (Residue form, k and n odd, 15 | k): ready Residue form, k and n odd, 15 | k erdos-1094--h3--h1--h2--h1--h2 (Residue form, k and n odd, 3 | k, 5 ∤ k, no carry at 5): ready Residue form, k and n odd, 3 | k, 5 ∤ k, no carry at 5 erdos-1094--h3--h1--h2--h2 (Residue form, k and n odd, 3 ∤ k, no carry at 3): ready Residue form, k and n odd, 3 ∤ k, no carry at 3 erdos-1094--h3--h1--h2--h2--h1 (Residue form, k and n odd, k ≡ 1 (mod 3)): ready Residue form, k and n odd, k ≡ 1 (mod 3) erdos-1094--h3--h1--h2--h2--h2 (Residue form, k and n odd, k ≡ n ≡ 2 (mod 3)): ready Residue form, k and n odd, k ≡ n ≡ 2 (mod 3) erdos-1094--h3--h1--h2--h2--h2--h1 (k divisible by 5): ready k divisible by 5 erdos-1094--h3--h1--h2--h2--h2--h2 (5 gives no carry): ready 5 gives no carry erdos-1094--h3--h2 (ELS lower bound: k² ≤ C·n·log₂k when lpf C(n,k) > k): ready ELS lower bound: k² ≤ C·n·log₂k when lpf C(n,k) > k erdos-1094--h3--h2--h1 (Ecklund–Erdős–Selfridge: n > k^(1+c) when lpf C(n,k) > k): ready Ecklund–Erdős–Selfridge: n > k^(1+c) when lpf C(n,k) > k Literature: known (proposed by t1016-lit, awaits confirmation) erdos-1094--h3--h2--h1--h1 (EES bound below k squared): needs-witness EES bound below k squared erdos-1094--h3--h2--h2 (ELS case B: k^(1+c) < n < k^(7/4), a prime in (k/2, k)): ready ELS case B: k^(1+c) < n < k^(7/4), a prime in (k/2, k) Literature: known (proposed by t1016-lit, awaits confirmation) erdos-1094--h3--h2--h3 (ELS case A: k^(7/4) ≤ n ≪ k²/log k, a prime in (k/2, k)): ready ELS case A: k^(7/4) ≤ n ≪ k²/log k, a prime in (k/2, k) Literature: known (proposed by t1016-lit, awaits confirmation) erdos-1094--h3--h3 (Granville–Ramaré: a carry at some prime p in (k/2, 11k/20)): ready Granville–Ramaré: a carry at some prime p in (k/2, 11k/20) 1 erdos-1094--h3--h3--h1 (Chebyshev sum of log p over (k/2, 11k/20) is at least k/100): ready Chebyshev sum of log p over (k/2, 11k/20) is at least k/100 erdos-1094--h3--h3--h1--h1 (Prime number theorem: θ(x) ~ x): ready Prime number theorem: θ(x) ~ x Literature: known (proposed by t1016-lit, awaits confirmation) erdos-1094--h3--h3--h1--h1--h1 (Prime number theorem for psi): ready Prime number theorem for psi erdos-1094--h3--h3--h1--h1--h1--h1 (Wiener–Ikehara Tauberian theorem): ready Wiener–Ikehara Tauberian theorem erdos-1094--h3--h3--h1--h1--h1--h2 (-ζ'/ζ minus the pole extends to Re s ≥ 1): ready -ζ'/ζ minus the pole extends to Re s ≥ 1 erdos-1094--h3--h3--h2 (Sander equidistribution: Σ({n/p} − 1/2) log p = o(k)): ready Sander equidistribution: Σ({n/p} − 1/2) log p = o(k) erdos-1094--h3--h3--h2--h1 (GR Lemma 5.1: {n/p} below σ carries weight σ Σ log p + o(k)): ready GR Lemma 5.1: {n/p} below σ carries weight σ Σ log p + o(k) Literature: known (proposed by t1016-lit, awaits confirmation) route erdos-1094@1: 3 holes, all needed; from attempts/20261008T130306Z-t1008-a-partial.lean route erdos-1094--h2@1: 2 holes, all needed; from attempts/20261009T124800Z-t1009-b-partial.lean route erdos-1094--h2--h1@1: 1 hole, all needed; from attempts/20261009T143300Z-t1009-c-partial.lean route erdos-1094--h2--h1--h1@1: 1 hole, all needed; from attempts/20261014T111741Z-t1014-y-partial.lean route erdos-1094--h2--h1--h1--h1@1: 2 holes, all needed; from attempts/20261015T151456Z-t1015c-a06-partial.lean route erdos-1094--h2--h1--h1--h1--h1@1: 2 holes, all needed; from attempts/20261018T192600Z-t1018-a-partial.lean route erdos-1094--h2--h1--h1--h1--h2@1: 2 holes, all needed; from attempts/20261018T193800Z-t1018-a-partial.lean route erdos-1094--h2--h1@2: 3 holes, all needed; from attempts/20261014T075000Z-t1014-a-partial.lean route erdos-1094--h2--h2--h2@1: 4 holes, all needed; from attempts/20261014T111800Z-t1014-x-partial.lean route erdos-1094--h2--h2--h2--h2@1: 1 hole, all needed; from attempts/20261014T181000Z-t1014-r-partial.lean route erdos-1094--h2--h2--h2--h3@1: 1 hole, all needed; from attempts/20261015T021346Z-t1015-r-partial.lean route erdos-1094--h2--h2--h2--h3--h1@1: 1 hole, all needed; from attempts/20261015T023339Z-t1015-r-partial.lean route erdos-1094--h2--h2--h2--h3--h1--h1@1: 1 hole, all needed; from attempts/20261015T063320Z-opn-prove-aristotle-1015-partial.lean route erdos-1094--h2--h2--h2--h3--h1--h1--h1@1: 1 hole, all needed; from attempts/20261015T130229Z-t1015b-s-partial.lean route erdos-1094--h2--h2--h2--h4@1: 1 hole, all needed; from attempts/20261015T023100Z-t1015-q-partial.lean route erdos-1094--h2--h1--h4@1: 1 hole, all needed; from attempts/20261014T111658Z-t1014-y-partial.lean route erdos-1094--h2--h1--h4--h1@1: 2 holes, all needed; from attempts/20261015T145300Z-t1015c-a06-partial.lean route erdos-1094--h2--h1--h4--h1--h2@1: 1 hole, all needed; from attempts/20261018T192800Z-t1018-b-partial.lean route erdos-1094--h2--h2@1: 3 holes, all needed; from attempts/20261014T073500Z-t1014-a-partial.lean route erdos-1094--h2--h2--h3@1: 1 hole, all needed; from attempts/20261014T111449Z-t1014-y-partial.lean route erdos-1094--h2--h2--h3--h1@1: 1 hole, all needed; from attempts/20261015T144930Z-t1015c-a08-partial.lean route erdos-1094--h3@1: 1 hole, all needed; from attempts/20261008T133001Z-t1008-a-partial.lean route erdos-1094--h3--h1@1: 2 holes, all needed; from attempts/20261009T125000Z-t1009-a-partial.lean route erdos-1094--h3--h1--h1@1: 2 holes, all needed; from attempts/20261014T112100Z-t1014-z-partial.lean route erdos-1094--h3--h1--h1--h1@1: 2 holes, all needed; from attempts/20261015T145000Z-t1015c-a12-partial.lean route erdos-1094--h3--h1--h1--h2@1: 1 hole, all needed; from attempts/20261014T175700Z-t1014-q-partial.lean route erdos-1094--h3--h1--h1--h2--h1@1: 2 holes, all needed; from attempts/20261015T145026Z-t1015c-a09-partial.lean route erdos-1094--h3--h1--h1@2: 1 hole, all needed; from attempts/20261015T145000Z-t1015c-a16-partial.lean route erdos-1094--h3--h1--h2@1: 2 holes, all needed; from attempts/20261014T112100Z-t1014-z-partial.lean route erdos-1094--h3--h1--h2--h1@1: 2 holes, all needed; from attempts/20261015T145000Z-t1015c-a10-partial.lean route erdos-1094--h3--h1--h2--h2@1: 2 holes, all needed; from attempts/20261015T145200Z-t1015c-a11-partial.lean route erdos-1094--h3--h1--h2--h2--h2@1: 2 holes, all needed; from attempts/20261018T192600Z-t1018-d-partial.lean route erdos-1094--h3@2: 1 hole, all needed; from attempts/20261009T143300Z-t1009-c-partial.lean route erdos-1094--h3@3: 2 holes, all needed; from attempts/20261015T125200Z-t1015b-g-partial.lean route erdos-1094--h3--h2@1: 3 holes, all needed; from attempts/20261015T132800Z-t1015b-h-partial.lean route erdos-1094--h3--h2--h1@1: 1 hole, all needed; from attempts/20261018T193200Z-t1018-c-partial.lean route erdos-1094--h3--h3@1: 2 holes, all needed; from attempts/20261015T132200Z-t1015b-g-partial.lean route erdos-1094--h3--h3--h1@1: 1 hole, all needed; from attempts/20261015T145500Z-t1015c-a03-partial.lean route erdos-1094--h3--h3--h1--h1@1: 1 hole, all needed; from attempts/20261018T192634Z-t1018-e-partial.lean route erdos-1094--h3--h3--h1--h1--h1@1: 2 holes, all needed; from attempts/20261018T200210Z-t1018-e-partial.lean route erdos-1094--h3--h3--h2@1: 1 hole, all needed; from attempts/20261015T145123Z-t1015c-a02-partial.lean
labels drop the problem’s own name (a pill’s title has its full id); hovertap a statement to light its lines; select a set in the tree above to see its tree here
Selected statement Erdős problem 1094

erdos-1094Rename or correct →

status
open
attempts
2 attempts

The problem's statement.

What is claimed

$\displaystyle \Bigl\{(n,k)\in\mathbb{N}^2 \;:\; 0<k,\ \ 2k\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \max\bigl(\lfloor n/k\rfloor,\,k\bigr)\Bigr\}\ \text{ is finite}$

  • $\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 $n > k > 0$, so $\binom{n}{k}\ge n\ge 2$ and $\operatorname{lpf}$ is the least prime factor.
  • 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 same holds inside the maximum.
  • The guard $0<k$ matters: Lean has n / 0 = 0 and $\binom{n}{0}=1$, so without it every pair $(n,0)$ would satisfy Nat.minFac 1 = 1 > max 0 0 and the set would be infinite.

In words: for $n\ge 2k$, the least prime factor of $\binom{n}{k}$ is at most $\max(n/k,\,k)$, with only finitely many exceptions.

unverified · history

Lean
theorem Opn.erdos_1094 :
    {(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite := by
  sorry

How it is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from these holes by 20261008T130306Z-t1008-a-partial.lean (merged in 305fb84fc6d8, attestation 000441).

  • h_fixed_k → erdos-1094--h1 (proved)

    $\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}$

  • h_large_n → erdos-1094--h2 (open)

    $\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$

  • h_small_n → erdos-1094--h3 (open)

    $\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^2,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$

Read the partial proof (Lean)
theorem Opn.erdos_1094 :
    {(n, k) : ℕ × ℕ | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite := by
  have hall : (∀ k : ℕ, 0 < k → {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}.Finite) ∧
      (∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k → (n.choose k).minFac > k → k ≤ K) := by
    refine ⟨?_, ?_, ?_⟩
    · have h_fixed_k : ∀ k : ℕ, 0 < k →
          {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}.Finite := by
        sorry
      exact h_fixed_k
    · have h_large_n : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n →
          (n.choose k).minFac > n / k → k ≤ K := by
        sorry
      exact h_large_n
    · have h_small_n : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → k ≤ K := by
        sorry
      exact h_small_n
  obtain ⟨hF, ⟨KA, hA⟩, ⟨KB, hB⟩⟩ := hall
  have hT : ∀ k ∈ Finset.Icc 1 (max KA KB),
      ({n : ℕ | n < k * k} ∪ {n : ℕ | k * k ≤ n ∧ (n.choose k).minFac > n / k}).Finite := by
    intro k hk
    exact (Set.finite_lt_nat (k * k)).union (hF k (Finset.mem_Icc.1 hk).1)
  refine (Set.Finite.biUnion (Finset.Icc 1 (max KA KB)).finite_toSet
    (fun k hk => (hT k hk).image (fun n => (n, k)))).subset ?_
  rintro ⟨n, k⟩ ⟨hk, h2k, hmin⟩
  rw [Set.mem_iUnion₂]
  by_cases hnk : k * k ≤ n
  · have hkd : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hnk
    have hmin' : (n.choose k).minFac > n / k := by rwa [max_eq_left hkd] at hmin
    have hbound : k ≤ max KA KB := le_trans (hA n k hk hnk hmin') (le_max_left _ _)
    exact ⟨k, Finset.mem_coe.2 (Finset.mem_Icc.2 ⟨hk, hbound⟩), n, Or.inr ⟨hnk, hmin'⟩, rfl⟩
  · have hlt : n < k * k := Nat.lt_of_not_le hnk
    have hdk : n / k ≤ k := le_of_lt ((Nat.div_lt_iff_lt_mul hk).2 hlt)
    have hmin' : (n.choose k).minFac > k := by rwa [max_eq_right hdk] at hmin
    have hbound : k ≤ max KA KB := le_trans (hB n k hk h2k hlt hmin') (le_max_right _ _)
    exact ⟨k, Finset.mem_coe.2 (Finset.mem_Icc.2 ⟨hk, hbound⟩), n, Or.inl hlt, rfl⟩

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094/attempts/20261008T130306Z-t1008-a-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems. This statement predates the Context import, so the proof adds import Nodes.«erdos-1094».Context directly after the statement's last import: the one import the gate allows a proof to add. A direct proof is accepted at any time.

What is known

Notes

  • Numerical checks of every statement of erdos-1094, 2026-10-12. full text →
  • Where the decomposition of the root stands on 2026-10-08, and the literature status of each piece. full text →
  • State of the problem, 2026-10-12. full text →

Work on it

Plans

  • Prior art and the state of the problem (Erdős #1094, the Erdős–Lacampagne–Selfridge conjecture), with a reading of the formal statement against it. — not followed by any merged decomposition · full text →

Approaches recorded as tried (D-14)

Work on this statement →
Record details (words, files)
hash
bbeff8af9bb8
origin
authored
mathlib
0df444a360ea
files
Statement.lean ↗

Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.

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

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. A gloss of a root is not its words of record: the curated statement above is (D-9).

Draft · drafted, by the model named above

$\displaystyle \Bigl\{(n,k)\in\mathbb{N}^2 \;:\; 0<k,\ \ 2k\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \max\bigl(\lfloor n/k\rfloor,\,k\bigr)\Bigr\}\ \text{ is finite}$

  • $\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 $n > k > 0$, so $\binom{n}{k}\ge n\ge 2$ and $\operatorname{lpf}$ is the least prime factor.
  • 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 same holds inside the maximum.
  • The guard $0<k$ matters: Lean has n / 0 = 0 and $\binom{n}{0}=1$, so without it every pair $(n,0)$ would satisfy Nat.minFac 1 = 1 > max 0 0 and the set would be infinite.

In words: for $n\ge 2k$, the least prime factor of $\binom{n}{k}$ is at most $\max(n/k,\,k)$, with only finitely many exceptions.

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

History: 2 versions on record

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

    Read this version

    The set of pairs (n, k) of natural numbers such that k is positive, n is at least 2k, and the least prime factor of the binomial coefficient C(n, k) is greater than both the floor of n/k and k, is finite.

    Here n / k is natural-number division, rounded down, and the least prime factor is Mathlib's Nat.minFac. Because the least prime factor is a whole number, exceeding the floor of n/k is the same as exceeding the real quotient n/k, so the statement says: for n at least 2k, the least prime factor of C(n, k) is at most max(n/k, k), with only finitely many exceptions.

  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 · gloss/7b7c4d3de4ae….md · diff to its predecessor

    Read this version

    $\displaystyle \Bigl\{(n,k)\in\mathbb{N}^2 \;:\; 0<k,\ \ 2k\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \max\bigl(\lfloor n/k\rfloor,\,k\bigr)\Bigr\}\ \text{ is finite}$

    • $\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 $n > k > 0$, so $\binom{n}{k}\ge n\ge 2$ and $\operatorname{lpf}$ is the least prime factor.
    • 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 same holds inside the maximum.
    • The guard $0<k$ matters: Lean has n / 0 = 0 and $\binom{n}{0}=1$, so without it every pair $(n,0)$ would satisfy Nat.minFac 1 = 1 > max 0 0 and the set would be infinite.

    In words: for $n\ge 2k$, the least prime factor of $\binom{n}{k}$ is at most $\max(n/k,\,k)$, with only finitely many exceptions.

Diff of 7b7c4d3de4ae against 0963b976a7a5
@@ -1,3 +1,7 @@
-The set of pairs (n, k) of natural numbers such that k is positive, n is at least 2k, and the least prime factor of the binomial coefficient C(n, k) is greater than both the floor of n/k and k, is finite.
+$$\Bigl\{(n,k)\in\mathbb{N}^2 \;:\; 0<k,\ \ 2k\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \max\bigl(\lfloor n/k\rfloor,\,k\bigr)\Bigr\}\ \text{ is finite}$$
 
-Here n / k is natural-number division, rounded down, and the least prime factor is Mathlib's Nat.minFac. Because the least prime factor is a whole number, exceeding the floor of n/k is the same as exceeding the real quotient n/k, so the statement says: for n at least 2k, the least prime factor of C(n, k) is at most max(n/k, k), with only finitely many exceptions.
+- $\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 $n > k > 0$, so $\binom{n}{k}\ge n\ge 2$ and $\operatorname{lpf}$ is the least prime factor.
+- `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 same holds inside the maximum.
+- The guard $0<k$ matters: Lean has `n / 0 = 0` and $\binom{n}{0}=1$, so without it every pair $(n,0)$ would satisfy `Nat.minFac 1 = 1 > max 0 0` and the set would be infinite.
+
+In words: for $n\ge 2k$, the least prime factor of $\binom{n}{k}$ is at most $\max(n/k,\,k)$, with only finitely many exceptions.

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

Outlines

Untrusted contributor text (D-31): an outline is an informal argument in named steps, not a proof. The full text is on the statement’s record page.

  • Prior art and the state of the problem (Erdős #1094, the Erdős–Lacampagne–Selfridge conjecture), with a reading of the formal statement… by t1008-c — not followed by any merged decomposition · full text →
Notes

Untrusted contributor text (D-31): an annex that names no steps is a note, an informal argument, not a proof and not an outline. The full text is on the statement’s record page.

  • annex/v1 note **Numerical checks of every statement of erdos-1094, 2026-10-12.** These are searches of finite ranges, not proofs. The code is at the end. by thisisanameforsure — not followed by any merged decomposition · full text →
  • annex/v1 note Where the decomposition of the root stands on 2026-10-08, and the literature status of each piece. A companion to the prior-art annex on… by t1008-c — not followed by any merged decomposition · full text →
  • annex/v1 note **State of the problem, 2026-10-12.** A summary of what the record holds for Erdős #1094 and what the literature is cited as saying. Each… by thisisanameforsure — not followed by any merged decomposition · full text →

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 a split, the partial proof assumes each and proves this statement from them. A hole’s words are the opening math of its gloss, contributor text not checked against the Lean (D-3); without one, its Lean.

How to read this →

8 ways to settle the problem, in the record’s order.

SetStatementsProvedOpenSharedAssembliesRoutes
Set 1
which

Open

  • h2--h1--h1--h1--h1--h1
  • h2--h1--h1--h1--h1--h2
  • h2--h1--h1--h1--h2--h1
  • h2--h1--h1--h1--h2--h2
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h1--h1--h1--h1
  • h3--h1--h1--h1--h2
  • h3--h1--h1--h2--h1--h1
  • h3--h1--h1--h2--h1--h2
  • h3--h1--h2--h1--h1
  • h3--h1--h2--h1--h2
  • h3--h1--h2--h2--h1
  • h3--h1--h2--h2--h2--h1
  • h3--h1--h2--h2--h2--h2

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h1
  • h2--h1--h1--h1
  • h2--h1--h1--h1--h1
  • h2--h1--h1--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h1
  • h3--h1--h1
  • h3--h1--h1--h1
  • h3--h1--h1--h2
  • h3--h1--h1--h2--h1
  • h3--h1--h2
  • h3--h1--h2--h1
  • h3--h1--h2--h2
  • h3--h1--h2--h2--h2
172621115172620erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@1erdos-1094--h2--h1--h1@1erdos-1094--h2--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@1erdos-1094--h3--h1@1erdos-1094--h3--h1--h1@1erdos-1094--h3--h1--h1--h1@1erdos-1094--h3--h1--h1--h2@1erdos-1094--h3--h1--h1--h2--h1@1erdos-1094--h3--h1--h2@1erdos-1094--h3--h1--h2--h1@1erdos-1094--h3--h1--h2--h2@1erdos-1094--h3--h1--h2--h2--h2@1
Set 2
which

Open

  • h2--h1--h1--h1--h1--h1
  • h2--h1--h1--h1--h1--h2
  • h2--h1--h1--h1--h2--h1
  • h2--h1--h1--h1--h2--h2
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h1--h1--h3
  • h3--h1--h2--h1--h1
  • h3--h1--h2--h1--h2
  • h3--h1--h2--h2--h1
  • h3--h1--h2--h2--h2--h1
  • h3--h1--h2--h2--h2--h2

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h1
  • h2--h1--h1--h1
  • h2--h1--h1--h1--h1
  • h2--h1--h1--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h1
  • h3--h1--h1
  • h3--h1--h2
  • h3--h1--h2--h1
  • h3--h1--h2--h2
  • h3--h1--h2--h2--h2
142321112142317erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@1erdos-1094--h2--h1--h1@1erdos-1094--h2--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@1erdos-1094--h3--h1@1erdos-1094--h3--h1--h1@2erdos-1094--h3--h1--h2@1erdos-1094--h3--h1--h2--h1@1erdos-1094--h3--h1--h2--h2@1erdos-1094--h3--h1--h2--h2--h2@1
Set 3
which

Open

  • h2--h1--h1--h1--h1--h1
  • h2--h1--h1--h1--h1--h2
  • h2--h1--h1--h1--h2--h1
  • h2--h1--h1--h1--h2--h2
  • h2--h2--h1
  • h2--h2--h3--h1--h1

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h1
  • h2--h1--h1--h1
  • h2--h1--h1--h1--h1
  • h2--h1--h1--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
817211681711erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@1erdos-1094--h2--h1--h1@1erdos-1094--h2--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@2
Set 4
which

Open

  • h2--h1--h1--h1--h1--h1
  • h2--h1--h1--h1--h1--h2
  • h2--h1--h1--h1--h2--h1
  • h2--h1--h1--h1--h2--h2
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h2--h1--h1
  • h3--h2--h2
  • h3--h2--h3
  • h3--h3--h1--h1--h1--h1
  • h3--h3--h1--h1--h1--h2
  • h3--h3--h2--h1

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h1
  • h2--h1--h1--h1
  • h2--h1--h1--h1--h1
  • h2--h1--h1--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h2
  • h3--h2--h1
  • h3--h3
  • h3--h3--h1
  • h3--h3--h1--h1
  • h3--h3--h1--h1--h1
  • h3--h3--h2
142321112142318erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@1erdos-1094--h2--h1--h1@1erdos-1094--h2--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@3erdos-1094--h3--h2@1erdos-1094--h3--h2--h1@1erdos-1094--h3--h3@1erdos-1094--h3--h3--h1@1erdos-1094--h3--h3--h1--h1@1erdos-1094--h3--h3--h1--h1--h1@1erdos-1094--h3--h3--h2@1
Set 5
which

Open

  • h2--h1--h4--h1--h1
  • h2--h1--h4--h1--h2--h1
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h1--h1--h1--h1
  • h3--h1--h1--h1--h2
  • h3--h1--h1--h2--h1--h1
  • h3--h1--h1--h2--h1--h2
  • h3--h1--h2--h1--h1
  • h3--h1--h2--h1--h2
  • h3--h1--h2--h2--h1
  • h3--h1--h2--h2--h2--h1
  • h3--h1--h2--h2--h2--h2

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h4
  • h2--h1--h4--h1
  • h2--h1--h4--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h1
  • h3--h1--h1
  • h3--h1--h1--h1
  • h3--h1--h1--h2
  • h3--h1--h1--h2--h1
  • h3--h1--h2
  • h3--h1--h2--h1
  • h3--h1--h2--h2
  • h3--h1--h2--h2--h2
152421113152419erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@2erdos-1094--h2--h1--h4@1erdos-1094--h2--h1--h4--h1@1erdos-1094--h2--h1--h4--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@1erdos-1094--h3--h1@1erdos-1094--h3--h1--h1@1erdos-1094--h3--h1--h1--h1@1erdos-1094--h3--h1--h1--h2@1erdos-1094--h3--h1--h1--h2--h1@1erdos-1094--h3--h1--h2@1erdos-1094--h3--h1--h2--h1@1erdos-1094--h3--h1--h2--h2@1erdos-1094--h3--h1--h2--h2--h2@1
Set 6
which

Open

  • h2--h1--h4--h1--h1
  • h2--h1--h4--h1--h2--h1
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h1--h1--h3
  • h3--h1--h2--h1--h1
  • h3--h1--h2--h1--h2
  • h3--h1--h2--h2--h1
  • h3--h1--h2--h2--h2--h1
  • h3--h1--h2--h2--h2--h2

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h4
  • h2--h1--h4--h1
  • h2--h1--h4--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h1
  • h3--h1--h1
  • h3--h1--h2
  • h3--h1--h2--h1
  • h3--h1--h2--h2
  • h3--h1--h2--h2--h2
122121110122116erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@2erdos-1094--h2--h1--h4@1erdos-1094--h2--h1--h4--h1@1erdos-1094--h2--h1--h4--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@1erdos-1094--h3--h1@1erdos-1094--h3--h1--h1@2erdos-1094--h3--h1--h2@1erdos-1094--h3--h1--h2--h1@1erdos-1094--h3--h1--h2--h2@1erdos-1094--h3--h1--h2--h2--h2@1
Set 7
which

Open

  • h2--h1--h1--h1--h1--h1
  • h2--h1--h1--h1--h1--h2
  • h2--h1--h1--h1--h2--h1
  • h2--h1--h1--h1--h2--h2
  • h2--h1--h4--h1--h1
  • h2--h1--h4--h1--h2--h1
  • h2--h2--h1
  • h2--h2--h3--h1--h1

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h4
  • h2--h1--h4--h1
  • h2--h1--h4--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h2--h1--h1
  • h2--h1--h1--h1
  • h2--h1--h1--h1--h1
  • h2--h1--h1--h1--h2
10192118101914erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@2erdos-1094--h2--h1--h4@1erdos-1094--h2--h1--h4--h1@1erdos-1094--h2--h1--h4--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@2erdos-1094--h2--h1--h1@1erdos-1094--h2--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h1@1erdos-1094--h2--h1--h1--h1--h2@1
Set 8
which

Open

  • h2--h1--h4--h1--h1
  • h2--h1--h4--h1--h2--h1
  • h2--h2--h1
  • h2--h2--h3--h1--h1
  • h3--h2--h1--h1
  • h3--h2--h2
  • h3--h2--h3
  • h3--h3--h1--h1--h1--h1
  • h3--h3--h1--h1--h1--h2
  • h3--h3--h2--h1

Proved

  • h1
  • h2--h2--h2
  • h1
  • h2--h2--h2
  • h2--h2--h2--h1
  • h2--h2--h2--h2
  • h2--h2--h2--h2--h1
  • h2--h2--h2--h3
  • h2--h2--h2--h3--h1
  • h2--h2--h2--h3--h1--h1
  • h2--h2--h2--h3--h1--h1--h1
  • h2--h2--h2--h3--h1--h1--h1--h1
  • h2--h2--h2--h4

Assemblies

  • erdos-1094
  • h2
  • h2--h1
  • h2--h1--h4
  • h2--h1--h4--h1
  • h2--h1--h4--h1--h2
  • h2--h2
  • h2--h2--h3
  • h2--h2--h3--h1
  • h3
  • h3--h2
  • h3--h2--h1
  • h3--h3
  • h3--h3--h1
  • h3--h3--h1--h1
  • h3--h3--h1--h1--h1
  • h3--h3--h2
122121110122117erdos-1094@1erdos-1094--h2@1erdos-1094--h2--h1@2erdos-1094--h2--h1--h4@1erdos-1094--h2--h1--h4--h1@1erdos-1094--h2--h1--h4--h1--h2@1erdos-1094--h2--h2@1erdos-1094--h2--h2--h3@1erdos-1094--h2--h2--h3--h1@1erdos-1094--h3@3erdos-1094--h3--h2@1erdos-1094--h3--h2--h1@1erdos-1094--h3--h3@1erdos-1094--h3--h3--h1@1erdos-1094--h3--h3--h1--h1@1erdos-1094--h3--h3--h1--h1--h1@1erdos-1094--h3--h3--h2@1

Proved, explained, written up

Not resolved, so no digestion state yet (D-33 v3.17).

Steward

Panel

The problem’s stewards who have not lapsed. They decide together by motions, under the panel’s rules.

  • Michael Higgins thisisanameforsure · last act 2026-10-14

Write-up

No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.

Where the statement comes from

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

Sources and licences (D-10):

No statement-QA pass is recorded yet (D-9 v3.12).

Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-1094/graph.json.

A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 5 (B+), at or above the high grade (D-4 step 9, F14).

Does the Lean say the conjecture?

What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.

Subjectbacktranslationbriefcompileequivalencescreen-consequencescreen-falsescreen-negationscreen-statement
root————————

Documented external attempts counting toward D-9's M: 1 against the statement as it stands.

Catalog evidence (F14): score 5 (B+) for erdos:1094, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.

Catalog score 5: the reasons, in score points (not counts of attempts):

  • +2 attempted by AlphaProof Nexus (Feb 2026), not solved
  • +1 no misformalization issue ever filed
  • +1 Lean statement public for 180+ days
  • +1 no file-local definitions (Mathlib vocabulary only)

No misformalization issue on record. In the registry since 2025-12-10, last changed 2026-07-16, 4 commits.

No upstream drift on record (D-10 v3.12).

Approach records

State of the problem

No state-of-the-problem note yet (D-32).