DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

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

#math #lean #research #algorithms

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:

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)
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Both are decidable (Mathlib infrastructure).

2.2 Explicit witnesses for n = 2..20

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

n a b c 4abc = n(bc+ac+ab) check
2 1 2 2 16 = 16 ✓
3 1 4 12 192 = 192 ✓
4 2 3 6 144 = 144 ✓
5 2 4 20 640 = 640 ✓
6 2 7 42 2352 = 2352 ✓
7 2 15 210 25200 = 25200 ✓
8 3 7 42 3528 = 3528 ✓
9 3 10 90 10800 = 10800 ✓
10 3 16 240 46080 = 46080 ✓
11 3 34 1122 457776 = 457776 ✓
12 4 13 156 32448 = 32448 ✓
13 4 18 468 134784 = 134784 ✓
14 4 29 812 376768 = 376768 ✓
15 4 63 1260 1270080 = 1270080 ✓
16 5 21 420 176400 = 176400 ✓
17 5 30 510 306000 = 306000 ✓
18 5 48 720 691200 = 691200 ✓
19 5 114 570 1299600 = 1299600 ✓
20 6 31 930 692160 = 692160 ✓

All verified by decide in Lean 4.

2.3 Aggregate theorem 

theorem es_small_solvable :
    ∀ n : Nat, 2 ≤ n → n ≤ 20 → erdosStrausSolvable n
Enter fullscreen mode Exit fullscreen mode

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)
Enter fullscreen mode Exit fullscreen mode

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))
Enter fullscreen mode Exit fullscreen mode

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.

Top comments (0)