Erdős–Straus, reformulated multiplicatively

The conjecture

The Erdős–Straus conjecture (1948) asks whether, for every integer n > 1, the equation

4 / n = 1 / x + 1 / y + 1 / z

has a solution in positive integers x, y, z. It's been verified computationally for enormous n, but a proof remains open.

What I proved

I did not prove the conjecture. What I did prove — and formalise end-to-end in Lean4 — is that the classical statement is equal as a proposition to a multiplicative reformulation phrased entirely over primes p ≡ 1 (mod 4). So the conjecture holds iff the multiplicative form holds. The original reformulation was hand-derived; the Lean development is the machine-checked version of it.

The development is a chain of reductions; each link is its own lemma, and the headline ties them together:

• erdos_straus_nat_equiv — clear denominators: rational ⟺ 4·x·y·z = n·(x·y + x·z + y·z) over ℕ⁺.
• erdos_straus_1_mod_4 — it suffices to solve the conjecture for primes p ≡ 1 (mod 4).
• erdos_straus_nat_imp_mult — the hard direction: nat form ⇒ multiplicative form, built on a custom gcd factor decomposition (factor_form) and a squarefree–square split (squarefree_square_form).
• erdos_straus_mult_imp_nat — the converse construction.
• erdos_straus_mult_equiv — the main theorem, the equality of the two propositions.

The full chain compiles cleanly, is sorry-free, and rests only on the three standard axioms (propext, Classical.choice, Quot.sound).

A snippet

-- The headline theorem (ErdosStraus/ErdosStraus.lean):
-- the classical Erdős–Straus statement is equal as a proposition
-- to a multiplicative reformulation over primes p ≡ 1 (mod 4).
theorem erdos_straus_mult_equiv :
    erdos_straus_conj = erdos_straus_conj_mult := by
  apply propext
  constructor
  · intro h; exact erdos_straus_nat_imp_mult (erdos_straus_1_mod_4.mp h)
  · intro h; exact erdos_straus_1_mod_4.mpr (erdos_straus_mult_imp_nat h)

The two directions split across ErdosStrausNatImpMult.lean (the hard direction, ~the bulk of the development) and ErdosStraus.lean (the converse). Everything underneath is in ErdosStrausUtil.lean: the four statement forms, the rational⟺nat equivalence, the mod-4 reduction, and the gcd factor decomposition that does the actual work.

Notes on the build

Two infrastructure choices shaped the development more than the proof itself:

• Everything is over ℕ⁺, not ℕ. This comes with the benefit of leaving positivity goals out at the drawback of weaker support from mathlib. To combat this, there's a small library, PNatUtility.lean (~30 lemmas), filling the gap.
• In addition to the PNat library, A custom nify tactic, the ℕ⁺ analogue of mathlib's zify/qify, was created. It drops goals down to ℕ where mathlib is rich, and casts back. Truncated subtraction is the awkward bit; passing ≤/< facts in as hypotheses lets push_cast via PNat.sub_cast handle it.

Stack

Lean 4.29 mathlib 4.29 ℕ⁺ arithmetic Number theory

Source

Repository is local-only at the moment; happy to share on request.