FormalConjectures/ErdosProblems/931.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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 931

Reference: erdosproblems.com/931

Imports (1)
Imported by 1 file
  1. theorem Erdos931.erdos_931 Let $k_1 \geq k_2 \geq 3$ sorry line 39 source

    Source documentation

    Let $k_1 \geq k_2 \geq 3$. Are there only finitely many $n_2\geq n_1 + k_1$ such that $$ \prod_{1\leq i\leq k_1}(n_1 + i)\ \text{and}\ \prod_{1\leq j\leq k_2} (n_2 + j) $$ have the same prime factors?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, LE.le, Set.Finite, Prod, Set.ofPred, Erdos931.erdos_931.match_1, And, HAdd.hAdd, Eq, Finset, Nat.primeFactors, Finset.prod, Finset.Icc

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

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_931 : answer(sorry) ↔ ∀ᵉ (k₁ : ℕ) (k₂ ≥ 3), k₂ ≤ k₁ →
    { (n₁, n₂) | n₁ + k₁ ≤ n₂ ∧
      (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
      (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors }.Finite := by
…
  2. theorem Erdos931.erdos_931.variants.additional_condition Erdős thought perhaps if the two products have the same factors then $n_2 > 2(n_1 + k_1)$ sorry line 51 source

    Source documentation

    Erdős thought perhaps if the two products have the same factors then $n_2 > 2(n_1 + k_1)$. It is an open question whether this is true when allowing a finite number of counterexamples.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, LE.le, Set.Finite, Prod, Set.ofPred, Erdos931.erdos_931.match_1, And, HAdd.hAdd, HMul.hMul, Eq, Finset, Nat.primeFactors, Finset.prod, Finset.Icc

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

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_931.variants.additional_condition : answer(sorry) ↔ ∀ᵉ (k₁ : ℕ) (k₂ ≥ 3), k₂ ≤ k₁ →
    {(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧
      (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
      (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite := by
…
  3. theorem Erdos931.erdos_931.variants.additional_condition_nonempty In fact there exist counterexamples, like this one found by AlphaProof line 61 source

    Source documentation

    In fact there exist counterexamples, like this one found by AlphaProof.

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

    Statement uses: Exists, Nat, LE.le, OfNat.ofNat, Set.Nonempty, Prod, Set.ofPred, Erdos931.erdos_931.match_1, And, HAdd.hAdd, HMul.hMul, Eq, Finset, Nat.primeFactors, Finset.prod, Finset.Icc

    Proof uses: Exists.intro, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Membership.mem, Set, Prod.mk, Eq.mpr, id, Eq.trans, Prod.fst, Prod.snd, congrFun', congrArg, funext, congr, Finset.prod_Icc_succ_top, Mathlib.Meta.NormNum.isNat_add and 37 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    theorem erdos_931.variants.additional_condition_nonempty : ∃ (k₁ k₂ : ℕ), ∃ (_h₁ : k₂ ≤ k₁), ∃ (_h₂ : 3 ≤ k₂),
  {(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ n₂ ≤ 2 * (n₁ + k₁) ∧
      (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
      (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Nonempty := by
…
  4. theorem Erdos931.erdos_931.variants.exists_prime Erdős was unable to prove that if the two products have the same factors then there must exist a prime between $n_1$ and $n_2$ sorry line 75 source

    Source documentation

    Erdős was unable to prove that if the two products have the same factors then there must exist a prime between $n_1$ and $n_2$.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Eq, Finset, Nat.primeFactors, Finset.prod, Finset.Icc, Exists, And, Nat.Prime

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

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_931.variants.exists_prime (k₁ k₂ n₁ n₂ : ℕ) (h₁ : k₂ ≤ k₁) (h₂ : 3 ≤ k₂)
    (h₃ : n₁ + k₁ ≤ n₂) (h₄ : (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors =
      (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors) :
    ∃ (p : ℕ), p.Prime ∧ n₁ ≤ p ∧ p ≤ n₂ := by
…