therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 306

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

Number theoryAMS 11

Mathematical statement

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

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_306

Canonical source
Complete statement target, proof intentionally absentLean 4
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  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationerdosproblems.com/306background