FormalConjectures/ErdosProblems/306.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos306.erdos_306 Let $\frac a b\in \mathbb{Q}_{>0}$ with $b$ squarefree sorry line 44 source

   Source documentation

   Let $\frac a b\in \mathbb{Q}_{>0}$ with $b$ squarefree. Are there integers $1 < n_1 < \dots < n_k$, each the product of two distinct primes, such that $\frac{a}{b}=\frac{1}{n_1}+\cdots+\frac{1}{n_k}$?

   depends on sorry what this means

   Statement uses: Iff, True, Rat, LT.lt, OfNat.ofNat, Squarefree, Nat, Rat.den, Exists, Fin, HAdd.hAdd, And, Eq, StrictMono, Membership.mem, Finset, Finset.Icc, Fin.last, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors and 3 more

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

   48 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_306 : answer(sorry) ↔ ∀ (q : ℚ), 0 < q → Squarefree q.den →
       ∃ k : ℕ, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ StrictMono n ∧
       (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 2 ∧ Ω (n i) = 2) ∧
       q = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i) := by
   …

2. theorem Erdos306.erdos_306.variants.integer_three_primes Every positive integer can be expressed as an Egyptian fraction where each denominator is the product of three distinct primes sorry line 55 source

   Source documentation

   Every positive integer can be expressed as an Egyptian fraction where each denominator is the product of three distinct primes.

   depends on sorry what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, And, GT.gt, Fin, HAdd.hAdd, Eq, Fin.mk, Membership.mem, Finset, Finset.Icc, Fin.last, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, ArithmeticFunction.cardFactors, Rat, Finset.sum, HDiv.hDiv

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

   48 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

   theorem erdos_306.variants.integer_three_primes (m : ℕ) (h : 0 < m) :
       ∃ k > (0 : ℕ), ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧
       ∀ i, (hik : i < k) → n ⟨i, by omega⟩ < n ⟨(i + 1), by omega⟩ ∧
       (∀ i ∈ Finset.Icc 1 (Fin.last k), ω (n i) = 3 ∧ Ω (n i) = 3) ∧
       m = ∑ i ∈ Finset.Icc 1 (Fin.last k), (1 : ℚ) / (n i) := by
   …