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

5 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 307

Reference: erdosproblems.com/307

Imports (1)
Imported by 1 file
  1. theorem Erdos307.erdos_307 Are there two finite set of primes $P$ and $Q$ such that $$ 1 = \left( \sum_{p \in P} \frac{1}{p} \right) \left( \sum_{q \in Q} \frac{1}{q} \right) $$ ? sorry line 45 source

    Source documentation

    Are there two finite set of primes $P$ and $Q$ such that

    $$ 1 = \left( \sum_{p \in P} \frac{1}{p} \right) \left( \sum_{q \in Q} \frac{1}{q} \right) $$ ?

    Asked by Barbeau [Ba76].

    [Ba76] Barbeau, E. J., Computer challenge corner: Problem 477: A brute force program.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Finset, Nat, And, Membership.mem, Nat.Prime, Eq, Rat, OfNat.ofNat, HMul.hMul, Finset.sum, Inv.inv

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

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_307 : answer(sorry) ↔ ∃ P Q : Finset ℕ, (∀ p ∈ P, p.Prime) ∧ (∀ q ∈ Q, q.Prime) ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹) := by
…
  2. theorem Erdos307.erdos_307.variants.coprime Instead of asking for sets of primes, ask only that all elements in the sets be relatively coprime line 62 source

    Source documentation

    Instead of asking for sets of primes, ask only that all elements in the sets be relatively coprime.

    Cambie has found several examples when this weakened version is true. For example, $$ 1=\left(1+\frac{1}{5}\right)\left(\frac{1}{2}+\frac{1}{3}\right) $$ and $$ 1=\left(1+\frac{1}{41}\right)\left(\frac{1}{2}+\frac{1}{3}+\frac{1}{7}\right). $$

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

    Statement uses: Iff, True, Exists, Finset, Nat, And, Not, Membership.mem, Inter.inter, OfNat.ofNat, LT.lt, Finset.card, Set.Pairwise, Nat.Coprime, Eq, Rat, HMul.hMul, Finset.sum, Inv.inv

    Proof uses: id, Eq.mpr, Eq.trans, congrArg, funext, congrFun', true_iff, Exists.intro, Insert.insert, Singleton.singleton, of_eq_true, congr, eq_true_of_decide, Eq.refl, Bool, Bool.true, HDiv.hDiv, HAdd.hAdd, Finset.sum_insert, False and 25 more

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    theorem erdos_307.variants.coprime : answer(True) ↔ ∃ P Q : Finset ℕ, 0 ∉ P ∩ Q ∧ 1 < #P ∧ 1 < #Q ∧
    Set.Pairwise P Nat.Coprime ∧ Set.Pairwise Q Nat.Coprime ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹) := by
…
  3. theorem Erdos307.erdos_307.variants.coprime_one_notMem There are no examples known of the weakened coprime version if we insist that $1\not\in P\cup Q$ sorry line 74 source

    Source documentation

    There are no examples known of the weakened coprime version if we insist that $1\not\in P\cup Q$.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Finset, Nat, And, Not, Membership.mem, Inter.inter, OfNat.ofNat, Union.union, LT.lt, Finset.card, Set.Pairwise, Nat.Coprime, Eq, Rat, HMul.hMul, Finset.sum, Inv.inv

    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_307.variants.coprime_one_notMem : answer(sorry) ↔ ∃ P Q : Finset ℕ, 0 ∉ P ∩ Q ∧ 1 ∉ P ∪ Q ∧
    1 < #P ∧ 1 < #Q ∧ Set.Pairwise P Nat.Coprime ∧ Set.Pairwise Q Nat.Coprime ∧
    1 = (∑ p ∈ P, (p : ℚ)⁻¹) * (∑ q ∈ Q, (q : ℚ)⁻¹) := by
…
  4. theorem Erdos307.erdos_307.barrier sorry line 90 source

    depends on sorry what this means

    Statement uses: Finset, Nat, Membership.mem, Nat.Prime, Finset.Nonempty, Eq, Rat, OfNat.ofNat, HMul.hMul, Finset.sum, Inv.inv, And, LE.le, Finset.card, Union.union, HPow.hPow, Finset.prod

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

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Erdos307.erdos_307.barrier_sixty sorry line 106 source

    depends on sorry what this means

    Statement uses: Finset, Nat, Membership.mem, Nat.Prime, Eq, Rat, OfNat.ofNat, HMul.hMul, Finset.sum, Inv.inv, LE.le, Finset.card, Union.union

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

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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