Erdős-Straus Conjecture — Lean 4 Small-n Formalization + Infinite Mod-4 Family

This article is a re-publication of Rei-AIOS Paper 117 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

• Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19646899
• Internet Archive: https://archive.org/details/rei-aios-paper-117-1776562122798
• Harvard Dataverse: https://doi.org/10.7910/DVN/KC56RY
• GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Authors: Nobuki Fujimoto (ORCID 0009-0004-6019-9258), Claude Code (Lean 4 formalization)
Date: 2026-04-19
Status: DRAFT — partial formalization. Not a proof of the full conjecture.
License: CC-BY-4.0
Repository: fc0web/rei-aios
Key file: data/lean4-mathlib/CollatzRei/ErdosStraus.lean (22 theorems, 0 sorry)
Related: Paper 109 (S-category Ricci-flow attack, 2026-04-17).

Abstract

The Erdős-Straus conjecture (1948) states that for every integer n ≥ 2 there exist positive integers a, b, c with 4/n = 1/a + 1/b + 1/c. It is empirically verified for n < 10^17 (Salez and others) and closed for many residue classes, but remains open in full generality. We provide a Lean 4 Mathlib-native formalization with 22 zero-sorry theorems: explicit witnesses for all n ∈ [2, 20] found by brute-force search and verified via decide, plus a structural infinite family showing every multiple of 4 is solvable via the triple (3k, 3k, 3k) at n = 4k.

The implementation uses the integer-arithmetic form 4·a·b·c = n·(b·c + a·c + a·b) which is decidable, and an interval_cases aggregate derives solvability uniformly for n ∈ [2, 20]. Extending to arbitrary n requires the classical mod-residue-class analysis (Mordell, Terzi, Elsholtz) which is not re-formalized here.

Keywords: Erdős-Straus, unit fractions, Lean 4, Mathlib, formal verification.

1. Background

1.1 Statement

Erdős and Straus (1948) asked: is it true that for every n ≥ 2 there are positive integers a ≤ b ≤ c with 4/n = 1/a + 1/b + 1/c?

1.2 Clearing denominators

Multiplying through:

4 a b c = n (b c + a c + a b)

This is a pure integer identity and is the form we formalize.

1.3 Known partial results

• Empirically verified for n < 10^17.
• Completely handled for n ≡ 0, 1, 2, 3, 4, 5, 8, 11 (mod 840) — Mordell 1969 + Terzi 1971.
• Open residue classes: {1, 121, 169, 289, 361, 529} (mod 840) when combined with additional obstructions.
• Elsholtz-Tao (2013) showed the number of representations is unbounded for certain sparse n.

1.4 Paper 109 background (Rei 2026-04-17)

Paper 109 applied the Rei-AIOS Ricci-flow 3-category taxonomy and found that 84.3% of classifiable small n fall into Category S (stable). This paper formalizes the complementary direction: explicit Lean 4 witnesses at the small-n frontier.

2. Lean 4 formalization

File: data/lean4-mathlib/CollatzRei/ErdosStraus.lean. 22 theorems, 0 sorry, Mathlib v4.27.0.

2.1 Predicate

def erdosStraus (n a b c : Nat) : Prop :=
  0 < a ∧ 0 < b ∧ 0 < c ∧
  4 * a * b * c = n * (b * c + a * c + a * b)

def erdosStrausSolvable (n : Nat) : Prop :=
  ∃ a b c : Nat, erdosStraus n a b c

Both are decidable (Mathlib infrastructure).

2.2 Explicit witnesses for n = 2..20

Found by brute-force search (smallest a, then smallest b, c):

All verified by decide in Lean 4.

2.3 Aggregate theorem

theorem es_small_solvable :
    ∀ n : Nat, 2 ≤ n → n ≤ 20 → erdosStrausSolvable n

Proof: interval_cases n + per-case explicit triple. Elementary.

2.4 Structural infinite family

For multiples of 4, the universal triple is (3k, 3k, 3k):

theorem es_four_k (k : Nat) (hk : 1 ≤ k) :
    erdosStraus (4 * k) (3 * k) (3 * k) (3 * k)

theorem es_solvable_mul_four (k : Nat) (hk : 1 ≤ k) :
    erdosStrausSolvable (4 * k)

Verification: 4·(3k)³ = 108k³ = 4k·27k² = 4k·(3k·3k + 3k·3k + 3k·3k). Proved by ring.

This closes all multiples of 4 ≥ 4 (i.e., n ∈ {4, 8, 12, 16, 20, ...}) with a single uniform witness.

3. Summary theorem

theorem ErdosStraus_summary :
    (∀ n : Nat, 2 ≤ n → n ≤ 20 → erdosStrausSolvable n)
    ∧ (∀ k : Nat, 1 ≤ k → erdosStrausSolvable (4 * k))

Combined coverage:

• All n ∈ [2, 20] individually verified.
• All multiples of 4 (≥ 4) uniformly solvable via one triple.

4. Scope and limitations

What this paper does

1. 22 zero-sorry theorems: 19 explicit cases + aggregate + structural family + summary.
2. Mathlib v4.27.0 native.
3. Small-case "frontier" (n ≤ 20) concrete and machine-checkable.
4. Proves an infinite class (multiples of 4) uniformly.

What this paper does not

1. Does NOT prove the full conjecture. Open n residue classes remain (e.g., n ≡ 1 (mod 840) combined with specific constraints).
2. Does NOT re-prove the Mordell/Terzi residue-class coverage — this would need a much larger formalization.
3. Does NOT give new number-theoretic progress. The contribution is Lean 4 formalization, not new math.

Honest claim

This is an elementary Lean 4 snapshot of the small-n frontier plus one universal family. The Mathlib community does not currently have a coherent-sieve or residue-class-coverage library for Erdős-Straus-style partial results, which is why this paper stops at (2) above.

5. Connection to Paper 109

Paper 109 (2026-04-17) applied discrete Ollivier-Ricci flow to Erdős-Straus partition graphs and classified 84.3% of classifiable n as Category S. Paper 117 (present) provides the complementary direction: formal witnesses rather than flow-category labels.

6. Reproducibility

• data/lean4-mathlib/CollatzRei/ErdosStraus.lean
  • Build: cd data/lean4-mathlib && lake build CollatzRei.ErdosStraus
  • 22 theorems, 0 sorry, ~48s to build (interval_cases + ring elaboration)
• Brute-force witness search: tmp/find-erdos-straus.ts (removed post-verification; triples are embedded in the Lean file)

7. Future work

1. Extended witness table for n = 21..100 via compiled routine.
2. Residue-class coverage proof for n ≡ 0, 1, 2, 3, 4, 5, 8, 11 (mod 840) — requires substantial Mathlib modular-arithmetic development.
3. Integration with Paper 109 Ricci-flow: classify each of the 19 cases by Category S/M/E.
4. Paper 118 candidate: Erdős-Straus vs Collatz structural comparison (via Ricci-flow signatures).

Paper 117 draft prepared 2026-04-19 by Claude Code under Nobuki Fujimoto's direction. This is an elementary formalization paper; the full conjecture remains open. Rei-AIOS research programme.