Erdős Problem 242: Erdős–Straus Proof

[Suro-One]

What is the conjecture

The Erdős–Straus conjecture asks whether every fraction of the form 4/n (for integers n ≥ 2) can always be written as the sum of three unit fractions: 4/n = 1/x + 1/y + 1/z

Prerequisites needed

See: https://github.com/Suro-One/auro-zera_Erdos-Straus_proof/

AMS categories

• ams-11

Choose either option

• I plan on adding this conjecture to the repository (I might)
• This issue is up for grabs: I would like to see this conjecture added by somebody else

[mo271]

We already have a formalisation of the Erdős Strauss conjecture:
https://www.erdosproblems.com/forum/thread/242

https://github.com/google-deepmind/formal-conjectures/blob/1efd73f117f6216638894027d87804d175e6b187/FormalConjectures/ErdosProblems/242.lean

Is your plan to add a proof? Not that in this repo, adding long proofs is out of scope, but adding a link to a proof we soon be in scope (see #1851)

[Suro-One]

We already have a formalisation of the Erdős Strauss conjecture: https://www.erdosproblems.com/forum/thread/242

https://github.com/google-deepmind/formal-conjectures/blob/1efd73f117f6216638894027d87804d175e6b187/FormalConjectures/ErdosProblems/242.lean

Is your plan to add a proof? Not that in this repo, adding long proofs is out of scope, but adding a link to a proof we soon be in scope (see #1851)

Yes