FormalConjectures/ErdosProblems/891.lean

GitHub source file

4 declarations, 4 contain sorry, 0 declared as axioms

1. theorem Erdos891.erdos_891 Let $2=p_1 < p_2 < \cdots$ be the primes and $k\geq 2$ sorry line 42 source

   Source documentation

   Let $2=p_1 < p_2 < \cdots$ be the primes and $k\geq 2$. Is it true that, for all sufficiently large $n$, there must exist an integer in $[n,n+p_1\cdots p_k)$ with $>k$ many prime factors?

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Filter.Eventually, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, Finset.prod, Finset.range, Nat.nth, Nat.Prime, LT.lt, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_891 :
       answer(sorry) ↔
         ∀ k ≥ 2, ∀ᶠ n in atTop,
         ∃ m ∈ Ico n (n + ∏ i ∈ range k, i.nth Nat.Prime), k < ω m := by
   …

2. theorem Erdos891.erdos_891.variants.schinzel Documented declaration: schinzel sorry line 53 source

   Source documentation

   Schinzel deduced from Pólya's theorem [Po18] (that the sequence of $k$-smooth integers has unbounded gaps) that this is true with $p_1\cdots p_k$ replaced by $p_1\cdots p_{k-1}p_{k+1}$.

   depends on sorry what this means

   Statement uses: Nat, GE.ge, OfNat.ofNat, Filter.Eventually, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, HMul.hMul, Finset.prod, Finset.range, HSub.hSub, Nat.nth, Nat.Prime, LT.lt, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_891.variants.schinzel :
       ∀ k ≥ 2, ∀ᶠ n in atTop,
         ∃ m ∈ Ico n (n + (∏ i ∈ range (k - 1), i.nth Nat.Prime) * k.nth Nat.Prime),
         k < ω m := by
   …

3. theorem Erdos891.erdos_891.variants.case_k_2 This is unknown even for $k=2$ - that is, is it true that in every interval of $6$ (sufficiently large) consecutive integers there must exist one with at least $3$ prime factors? sorry line 64 source

   Source documentation

   This is unknown even for $k=2$ - that is, is it true that in every interval of $6$ (sufficiently large) consecutive integers there must exist one with at least $3$ prime factors?

   depends on sorry what this means

   Statement uses: Iff, True, Filter.Eventually, Nat, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, OfNat.ofNat, LE.le, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_891.variants.case_k_2 :
       answer(sorry) ↔ ∀ᶠ n in atTop,
         ∃ m ∈ Ico n (n + 6), 3 ≤ ω m := by
   …

4. theorem Erdos891.erdos_891.variants.weisenberg Weisenberg has observed that Dickson's conjecture implies the answer is no if we replace $p_1\cdots p_k$ with $p_1\cdots p_k-1$ sorry line 80 source

   Source documentation

   Weisenberg has observed that Dickson's conjecture implies the answer is no if we replace $p_1\cdots p_k$ with $p_1\cdots p_k-1$. Indeed, let $L_k$ be the lowest common multiple of all integers at most $p_1\cdots p_k$. By Dickson's conjecture [Wikipedia], there are infinitely many $n'$ such that $\frac{L_k}{m}n'+1$ is prime for all $1\leq m < p_1\cdots p_k$. It follows that, if $n=L_kn'+1$, then all integers in $[n,n+p_1\cdots p_k-1)$ have at most $k$ prime factors.

   The statement is conditional on Dickson's conjecture, formalised as Dickson.dickson_conjecture.

   depends on sorry what this means

   Statement uses: Nat, GE.ge, OfNat.ofNat, Finset, Polynomial, Int, Membership.mem, And, Eq, WithBot, Polynomial.degree, BunyakovskyCondition, SchinzelCondition, Infinite, Set.ofPred, Nat.Prime, Int.natAbs, Polynomial.eval, Filter.Frequently, Finset.Ico and 9 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_891.variants.weisenberg (k : ℕ) (hk : k ≥ 2)
       (hdickson : type_of% Dickson.dickson_conjecture) :
       ∃ᶠ n in atTop,
         ∀ m ∈ Ico n (n + (∏ i ∈ range k, i.nth Nat.Prime) - 1),
         ω m ≤ k := by
   …

   Mentions: Dickson.dickson_conjecture