700.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

15 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 700

Reference: erdosproblems.com/700

A problem of Erdős and Szekeres [ErSz78].

References:

[ErSz78] Erdős, P. and Szekeres, G., Some number theoretic problems on binomial coefficients, Austral. Math. Soc. Gaz. (1978), 97-99.
OEIS A091963
Guy, R. K., Unsolved Problems in Number Theory, B31, B33.

Imports (1)

FormalConjecturesUtil

def Erdos700.f f n = min_{1 < k ≤ n/2} gcd(n, C(n,k)) line 42 source
Source documentation
f n = min_{1 < k ≤ n/2} gcd(n, C(n,k)). (The infimum is 0 when the range is empty, i.e. n < 4.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, And, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, Eq, Nat.gcd, Nat.choose
6 instances, coercions and auxiliary constants left out.
```
noncomputable def f (n : ℕ) : ℕ :=
…
```
def Erdos700.P P n is the largest prime factor of n (and 0 if n ≤ 1) line 46 source
Source documentation
P n is the largest prime factor of n (and 0 if n ≤ 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sup, Nat.primeFactors, id
3 instances, coercions and auxiliary constants left out.
```
noncomputable def P (n : ℕ) : ℕ := n.primeFactors.sup id
```
def Erdos700.Q $Q(n)$ is the largest prime-power divisor of $n$: the maximum of $p^{v_p(n)}$ over prime divisors $p$ of $n$ line 50 source
Source documentation
$Q(n)$ is the largest prime-power divisor of $n$: the maximum of $p^{v_p(n)}$ over prime divisors $p$ of $n$. It is 0 when n ≤ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sup, Nat.primeFactors, HPow.hPow, Finsupp, Nat.factorization
11 instances, coercions and auxiliary constants left out.
```
noncomputable def Q (n : ℕ) : ℕ := n.primeFactors.sup (fun p => p ^ n.factorization p)
```
def Erdos700.fSet The set whose infimum defines f line 53 source
Source documentation
The set whose infimum defines f.

no axioms what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Exists, And, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, Eq, Nat.gcd, Nat.choose
5 instances, coercions and auxiliary constants left out.
```
def fSet (n : ℕ) : Set ℕ := {m | ∃ k, 1 < k ∧ k ≤ n / 2 ∧ m = Nat.gcd n (n.choose k)}
…
```
lemma Erdos700.f_eq f n unfolds to the infimum of fSet n line 57 source
Source documentation
f n unfolds to the infimum of fSet n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos700.f, InfSet.sInf, Erdos700.fSet
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
```
lemma f_eq (n : ℕ) : f n = sInf (fSet n) := rfl
…
```
Mentions: Erdos700.f, Erdos700.fSet
lemma Erdos700.f_mem Each gcd(n, C(n,k)) with 1 < k ≤ n/2 belongs to fSet n line 61 source
Source documentation
Each gcd(n, C(n,k)) with 1 < k ≤ n/2 belongs to fSet n.

no axioms what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, Membership.mem, Set, Erdos700.fSet, Nat.gcd, Nat.choose
Proof uses: Exists.intro, And, Eq, And.intro, rfl
11 instances, coercions and auxiliary constants left out.
```
lemma f_mem (n k : ℕ) (h1 : 1 < k) (h2 : k ≤ n / 2) :
    Nat.gcd n (n.choose k) ∈ fSet n := ⟨k, h1, h2, rfl⟩
…
```
Mentions: Erdos700.fSet
lemma Erdos700.f_le f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2 line 66 source
Source documentation
f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, Erdos700.f, Nat.gcd, Nat.choose
Proof uses: Nat.sInf_le, Set.ofPred, Exists, And, Eq, Erdos700.f_mem
10 instances, coercions and auxiliary constants left out.
```
lemma f_le (n k : ℕ) (h1 : 1 < k) (h2 : k ≤ n / 2) :
    f n ≤ Nat.gcd n (n.choose k) := Nat.sInf_le (f_mem n k h1 h2)
…
```
Mentions: Erdos700.f, Erdos700.f_mem
theorem Erdos700.erdos_700.parts.i Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$ and let $P(n)$ be the largest prime dividing $n$ sorry line 82 source
Source documentation
Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$ and let $P(n)$ be the largest prime dividing $n$.
(a) Characterise those composite $n$ such that $f(n) = n/P(n)$.
Erdős–Szekeres [ErSz78] note that $f(n) = n/P(n)$ when $n$ is a product of two primes (erdos_700.variants.prime_mul), with $n = 30$ a further example. The characterisation itself is open; we state it as the (unknown) set of all composite n with f n = n / P n.
This follows the largest-prime reading on erdosproblems.com. In [ErSz78, p. 98], the first prose line below (7) reads: "where $P(n)$ is the greatest prime power which divides $n$." The paper's reading is stated with $Q(n)$ in erdos_700.variants.prime_power_divisor.

depends on sorry what this means
Statement uses: Eq, Set, Nat, Set.ofPred, And, Not, Nat.Prime, LT.lt, OfNat.ofNat, Erdos700.f, HDiv.hDiv, Erdos700.P, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.parts.i :
    {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ f n = n / P n} = answer(sorry) := by
…
```
Mentions: Erdos700.f, Erdos700.P
theorem Erdos700.erdos_700.variants.prime_power_divisor Characterise those composite $n$ such that $f(n) = n/Q(n)$, where $Q(n)$ is the largest prime-power divisor of $n$ sorry line 90 source
Source documentation
Characterise those composite $n$ such that $f(n) = n/Q(n)$, where $Q(n)$ is the largest prime-power divisor of $n$. This is the reading of part (a) in Erdős–Szekeres ErSz78, pp. 98–99.

L4DEL explanation
Characterise those composite $n$ such that $f(n) = n/Q(n)$, where $Q(n)$ is the largest prime-power divisor of $n$. This is the reading of part (a) in Erdős–Szekeres ErSz78, pp. 98–99.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Eq, Set, Nat, Set.ofPred, And, Not, Nat.Prime, LT.lt, OfNat.ofNat, Erdos700.f, HDiv.hDiv, Erdos700.Q, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.variants.prime_power_divisor :
    {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ f n = n / Q n} = answer(sorry) := by
…
```
Mentions: Erdos700.f, Erdos700.Q
theorem Erdos700.prime_power_divisor_separation At $n = 12$, $f(n) = 3 = n/Q(n)$, whereas $n/P(n) = 4$ line 96 source
Source documentation
At $n = 12$, $f(n) = 3 = n/Q(n)$, whereas $n/P(n) = 4$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Nat, Erdos700.f, OfNat.ofNat, HDiv.hDiv, Erdos700.P, Erdos700.Q
Proof uses: And.intro, le_antisymm, Erdos700.f_le, of_decide_eq_true, LT.lt, id, Bool, Decidable.decide, Bool.true, Eq.refl, LE.le, Set.Nonempty, Erdos700.fSet, Exists.intro, Membership.mem, Set, Nat.gcd, Nat.choose, Erdos700.f_mem, InfSet.sInf and 15 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem prime_power_divisor_separation : f 12 = 3 ∧ 12 / P 12 = 4 ∧ 12 / Q 12 = 3 := by
…
```
Mentions: Erdos700.f, Erdos700.P, Erdos700.Q
theorem Erdos700.erdos_700.parts.ii Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$ sorry line 116 source
Source documentation
Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$.
(b) Are there infinitely many composite $n$ such that $f(n) > n^{1/2}$?
Erdős–Szekeres [ErSz78] could not prove this. (Since $f(n) \ge p(n)$, the least prime factor of $n$, there are infinitely many $n$ — those of the form $p^2$ — with $f(n) \ge n^{1/2}$; the question asks for the strict inequality.) Here $f(n) > n^{1/2}$ is written as (f n) ^ 2 > n.

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, And, Not, Nat.Prime, LT.lt, OfNat.ofNat, GT.gt, HPow.hPow, Erdos700.f
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.parts.ii :
    answer(sorry) ↔ {n : ℕ | ¬ n.Prime ∧ 1 < n ∧ (f n) ^ 2 > n}.Infinite := by
…
```
Mentions: Erdos700.f
theorem Erdos700.erdos_700.parts.iii Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$ sorry line 128 source
Source documentation
Let $f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k})$.
(c) Is it true that, for every composite $n$, $f(n) \ll_A n/(\log n)^A$ for every $A > 0$?
Erdős–Szekeres [ErSz78] prove the weaker bound $f(n) \le (1 + o(1)) n/\log n$ (the case $A = 1$). Here $f(n) \ll_A n/(\log n)^A$ is spelled out as: for every A > 0 there is a constant C (depending on A) with f(n) ≤ C · n/(log n)^A for every composite n.

depends on sorry what this means
Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Exists, And, Nat, Not, Nat.Prime, LE.le, Erdos700.f, HDiv.hDiv, HMul.hMul, HPow.hPow, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.parts.iii :
    answer(sorry) ↔ (∀ A : ℝ, 0 < A → ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, ¬ n.Prime → 1 < n →
      (f n : ℝ) ≤ C * (n : ℝ) / (Real.log n) ^ A) := by
…
```
Mentions: Erdos700.f
lemma Erdos700.prime_dvd_of_not_dvd_choose Lucas (one step): for prime P ∣ n, if P ∤ C(n,k) then P ∣ k line 137 source
Source documentation
Lucas (one step): for prime P ∣ n, if P ∤ C(n,k) then P ∣ k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Dvd.dvd, Not, Nat.choose
Proof uses: Fact, Fact.mk, Decidable.byContradiction, Nat.ModEq, HMul.hMul, HMod.hMod, HDiv.hDiv, Choose.choose_modEq_choose_mod_mul_choose_div_nat, Eq, OfNat.ofNat, Iff.mpr, Nat.modEq_zero_iff_dvd, LT.lt, Nat.pos_of_ne_zero, Nat.dvd_of_mod_eq_zero, Iff.mp, Eq.mp, congrArg, MulZeroClass.zero_mul, Nat.choose_eq_zero_of_lt
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma prime_dvd_of_not_dvd_choose (P n k : ℕ) (hP : P.Prime) (hPn : P ∣ n)
    (h : ¬ P ∣ n.choose k) : P ∣ k := by
…
```
Mentions: Erdos700.P
theorem Erdos700.erdos_700.variants.prime_pow f(p^a) = p for a prime p and a ≥ 2 (recorded by Erdős–Szekeres [ErSz78]) line 154 source
Source documentation
f(p^a) = p for a prime p and a ≥ 2 (recorded by Erdős–Szekeres [ErSz78]). In particular, since (p^a) / P(p^a) = p^{a-1}, the prime power p^a is a "hit" (f(n) = n / P(n)) if and only if a = 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Eq, Erdos700.f, HPow.hPow
Proof uses: Nat.Prime.two_le, HSub.hSub, rfl, Ne, LT.lt.ne', pow_pos, Nat.Prime.pos, Nat.pow_le_pow_right, Decidable.byContradiction, Not, LT.lt, Trans.trans, Nat.Prime.one_lt, Nat.le_self_pow, HDiv.hDiv, HMul.hMul, Eq.mpr, id, congrArg, HAdd.hAdd and 63 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.variants.prime_pow (p a : ℕ) (hp : p.Prime) (ha : 2 ≤ a) : f (p ^ a) = p := by
…
```
Mentions: Erdos700.f
theorem Erdos700.erdos_700.variants.prime_mul f(pq) = p for distinct primes p < q (recorded by Erdős–Szekeres [ErSz78]); in particular pq is always a "hit" (f(pq) = pq / P(pq) = p) line 210 source
Source documentation
f(pq) = p for distinct primes p < q (recorded by Erdős–Szekeres [ErSz78]); in particular pq is always a "hit" (f(pq) = pq / P(pq) = p). Proof via Lucas' theorem: p ∤ C(pq,k) ⟹ p ∣ k (and the same for q), so any k with gcd(pq, C(pq,k)) = 1 must be a multiple of pq, of which there are none in (1, pq/2]; the witness k = q gives gcd(pq, C(pq,q)) = p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, Eq, Erdos700.f, HMul.hMul
Proof uses: Fact, Fact.mk, LE.le, OfNat.ofNat, Nat.Prime.two_le, Not, Dvd.dvd, Iff.mp, Nat.prime_dvd_prime_iff_eq, Decidable.byContradiction, HDiv.hDiv, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq and 113 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 92 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_700.variants.prime_mul (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p < q) :
    f (p * q) = p := by
…
```
Mentions: Erdos700.f