The Erdős–Straus conjecture - unresolved root goal
OpenErdosStraus242.erdos_242egyptian-fractionsnumber-theory
For every natural number , there exist natural numbers with such that 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 with , there exist natural numbers , , and such that , , and , and . 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 , , and are distinct and positive. No conclusion is asserted for , , or .
Human review
Confirmed by the mission captain (proposal self-audit).