Erdős–Straus conjecture

TheoremType I Erdős–Straus triples from divisors of a square#●ready to prove

Let \(p\) be a prime and let \(x\) be a natural number with \(\lceil p/4 \rceil \le x \le \lceil p/2 \rceil\). If \(d\) is a positive divisor of \(x^2\) with \(d \equiv -px \pmod{4x - p}\), then there are natural numbers \(y\) and \(z\) with \((4x - p)\,y = px + d\) and \((4x - p)\,d\,z = px(px + d)\) such that \(x \le y \le z\) and \(p \nmid y\).

Since \(4x > p\), these equations say \(y = (px + d)/(4x - p)\) and \(z = p(x + px^2/d)/(4x - p)\).

public theorem_wanted erdosStraus_typeI_of_dvd_sq {p x d : ℕ} (hp : p.Prime)
    (hx₁ : (p + 3) / 4 ≤ x) (hx₂ : x ≤ (p + 1) / 2) (hd₀ : 0 < d) (hd : d ∣ x ^ 2)
    (hmod : (4 * x - p : ℤ) ∣ d + p * x) :
    ∃ y z : ℕ, (4 * x - p : ℤ) * y = p * x + d ∧ (4 * x - p : ℤ) * d * z = p * x * (p * x + d) ∧
      x ≤ y ∧ y ≤ z ∧ ¬ p ∣ y
Sources
  • Kyle Bradford, Elementary Patterns from the Erdős-Straus Conjecture, INTEGERS 25 (2025), Article A54, Proposition 1.

TheoremDivisor criterion necessary for type I Erdős–Straus solutions#●ready to prove

Let \(p\) be a prime and let \(x \le y \le z\) be positive integers with \(4/p = 1/x + 1/y + 1/z\) and \(p \nmid y\). Then \(\lceil p/4 \rceil \le x \le \lceil p/2 \rceil\), and there is a positive divisor \(d\) of \(x^2\) with \(d \equiv -px \pmod{4x - p}\), \((4x - p)\,y = px + d\) and \((4x - p)\,d\,z = px(px + d)\).

Since \(4x > p\), the last two equations say \(y = (px + d)/(4x - p)\) and \(z = p(x + px^2/d)/(4x - p)\).

public theorem_wanted erdosStraus_typeI_exists_dvd_sq {p x y z : ℕ} (hp : p.Prime) (hx : 0 < x)
    (hxy : x ≤ y) (hyz : y ≤ z) (h : (4 : ℚ) / p = 1 / x + 1 / y + 1 / z) (hpy : ¬ p ∣ y) :
    (p + 3) / 4 ≤ x ∧ x ≤ (p + 1) / 2 ∧
      ∃ d : ℕ, 0 < d ∧ d ∣ x ^ 2 ∧ (4 * x - p : ℤ) ∣ d + p * x ∧
        (4 * x - p : ℤ) * y = p * x + d ∧ (4 * x - p : ℤ) * d * z = p * x * (p * x + d)
Sources
  • Kyle Bradford, Elementary Patterns from the Erdős-Straus Conjecture, INTEGERS 25 (2025), Article A54, Proposition 3.

TheoremDivisor criterion necessary for type II Erdős–Straus solutions#●ready to prove

Let \(p\) be a prime and let \(x \le y \le z\) be positive integers with \(4/p = 1/x + 1/y + 1/z\) and \(p \mid y\). Then \(\lceil p/4 \rceil \le x \le \lceil p/2 \rceil\), and there is a positive divisor \(d\) of \(x^2\) with \(d \le x\), \(d \equiv -x \pmod{4x - p}\), \((4x - p)\,y = p(x + d)\) and \((4x - p)\,d\,z = px(x + d)\).

Since \(4x > p\), the last two equations say \(y = p(x + d)/(4x - p)\) and \(z = p(x + x^2/d)/(4x - p)\).

public theorem_wanted erdosStraus_typeII_exists_dvd_sq {p x y z : ℕ} (hp : p.Prime) (hx : 0 < x)
    (hxy : x ≤ y) (hyz : y ≤ z) (h : (4 : ℚ) / p = 1 / x + 1 / y + 1 / z) (hpy : p ∣ y) :
    (p + 3) / 4 ≤ x ∧ x ≤ (p + 1) / 2 ∧
      ∃ d : ℕ, 0 < d ∧ d ∣ x ^ 2 ∧ d ≤ x ∧ (4 * x - p : ℤ) ∣ d + x ∧
        (4 * x - p : ℤ) * y = p * (x + d) ∧ (4 * x - p : ℤ) * d * z = p * x * (x + d)
Sources
  • Kyle Bradford, Elementary Patterns from the Erdős-Straus Conjecture, INTEGERS 25 (2025), Article A54, Proposition 4.

TheoremChamberland's characterization of restricted Erdős–Straus representations#●ready to prove

For a prime \(p\), there are positive integers \(a \le b \le c\) with \(p \nmid a\), \(p \mid b\), \(p \mid c\) and \(4/p = 1/a + 1/b + 1/c\) if and only if there are positive integers \(q\), \(r\), \(s_1\), \(s_2\) with \(q \equiv 3 \pmod 4\), both \(s_1\) and \(s_2\) dividing \((q + 1)/4\), and \(p + 4 s_1 s_2 = qr\).

theorem_wanted erdos_straus_prime_restricted_representation_iff
    (p : ℕ) (hp : p.Prime) :
    (∃ a b c : ℕ, 0 < a ∧ 0 < b ∧ 0 < c ∧ a ≤ b ∧ b ≤ c ∧
      ¬p ∣ a ∧ p ∣ b ∧ p ∣ c ∧
      (4 : ℚ) / p = 1 / a + 1 / b + 1 / c) ↔
    (∃ q r s₁ s₂ : ℕ, 0 < q ∧ 0 < r ∧ 0 < s₁ ∧ 0 < s₂ ∧
      q % 4 = 3 ∧ s₁ ∣ (q + 1) / 4 ∧ s₂ ∣ (q + 1) / 4 ∧
      p + 4 * s₁ * s₂ = q * r)
Sources
  • Marc Chamberland, "The Erdős-Straus Conjecture and the Structure of Primes", Theorem 1.
4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.