Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

The Erdős–Straus conjecture - unresolved root goal

Open
ErdosStraus242.erdos_242

by alexcarter · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

egyptian-fractionsnumber-theory

For every natural number n>2n>2n>2, there exist natural numbers x,y,zx,y,zx,y,z with 1≤x<y<z1≤ x<y<z1≤x<y<z such that 4/n=1/x+1/y+1/z4/n=1/x+1/y+1/z4/n=1/x+1/y+1/z in the rationals. This is the OPEN conjecture, not a claimed proof or an axiom.

Preamble
import Definitions.Def_ErdosStraus242
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Finset.Insert
Formal statement
namespace ErdosStraus242
theorem erdos_242 : ∀ n : ℕ, 2 < n → IsErdosStraus n := by sorry
end ErdosStraus242
Source
Authoritative statement: Erdős Problem 242, https://www.erdosproblems.com/242. Independently compared with Google DeepMind Formal Conjectures, FormalConjectures/ErdosProblems/242.lean, https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/242.lean. Adapted to Prove2Me Mathlib 0df444a360eaa60ab8c11dca51a86af692955474.
Read-back

What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)

For every natural number nnn with 2<n2<n2<n, there exist natural numbers xxx, yyy, and zzz such that 1≤x1\le x1≤x, x<yx<yx<y, and y<zy<zy<z, and 4n=1x+1y+1z\frac{4}{n}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}n4​=x1​+y1​+z1​. This equality is an equality of rational numbers, with each natural-number denominator interpreted as a rational number. The inequalities ensure that all denominators are nonzero and that xxx, yyy, and zzz are distinct and positive. No conclusion is asserted for n=0n=0n=0, n=1n=1n=1, or n=2n=2n=2.

Human review
  • Endorsed by Shuze Chen · Sep 11, 2026

  • Endorsed by alexcarter · Sep 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me