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.