FormalConjectures/ErdosProblems/1093.lean

GitHub source file

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

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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1093

Reference: erdosproblems.com/1093

Imports (1)
Imported by 1 file
  1. def Erdos1093.deficiency If defined, the deficiency is the count of $0 \le i < k$ such that $n - i$ is $k$-smooth, that is, divisible only by primes $\le k$ line 39 source

    Source documentation

    If defined, the deficiency is the count of $0 \le i < k$ such that $n - i$ is $k$-smooth, that is, divisible only by primes $\le k$.

    Nat.smoothNumbers m is the set of positive naturals all of whose prime factors are $< m$, so "$k$-smooth" in the sense above is Nat.smoothNumbers (k + 1).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: Finset.card, Finset.filter, Membership.mem, Set, Nat.smoothNumbers, HAdd.hAdd, OfNat.ofNat, HSub.hSub, Finset.range

    7 instances, coercions and auxiliary constants left out.

    noncomputable def deficiency (n k : ℕ) : ℕ :=
…
  2. theorem Erdos1093.erdos_1093.parts.i Are there infinitely many binomial coefficients with deficiency 1? sorry line 46 source

    Source documentation

    Are there infinitely many binomial coefficients with deficiency 1?

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Prod, Nat, Set.ofPred, Prod.fst, Prod.snd, And, LE.le, HMul.hMul, OfNat.ofNat, Eq, Erdos1093.deficiency, Nat.Prime, Dvd.dvd, Nat.choose, LT.lt

    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_1093.parts.i :
    answer(sorry) ↔ {x : ℕ × ℕ | let k := x.1; let n := x.2; 2 * k ≤ n ∧ deficiency n k = 1 ∧
…

    Mentions: Erdos1093.deficiency

  3. theorem Erdos1093.erdos_1093.parts.ii Are there only finitely many binomial coefficients with deficiency > 1? sorry line 55 source

    Source documentation

    Are there only finitely many binomial coefficients with deficiency > 1?

    depends on sorry what this means

    Statement uses: Set.Finite, Prod, Nat, Set.ofPred, Prod.fst, Prod.snd, And, LE.le, HMul.hMul, OfNat.ofNat, GT.gt, Erdos1093.deficiency, Nat.Prime, Dvd.dvd, Nat.choose, LT.lt

    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_1093.parts.ii :
    {x : ℕ × ℕ | let k := x.1; let n := x.2; 2 * k ≤ n ∧ deficiency n k > 1 ∧
…

    Mentions: Erdos1093.deficiency