939.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 939

References:

erdosproblems.com/939
[Ni95] Nitaj, A., On a conjecture of Erdős on 3-powerful numbers. Bull. London Math. Soc. (1995), 317-318.
[Co98] Cohn, J. H. E., A conjecture of Erdős on 3-powerful numbers. Math. Comp. (1998), 439-440.
[Wa24] Walsh, P., A question of Erdős on 3-powerful numbers and an elliptic curve analogue of the Ankeny-Artin-Chowla conjecture. arXiv:2404.03970 (2024).
[LaPa67] Lander, L. J. and Parkin, T. R., A counterexample to Euler's sum of powers conjecture. Math. Comp. (1967), 101-103.

Imports (1)

FormalConjecturesUtil

def Erdos939.Erdos939Sums A set S belongs to Erdos939Sums r if it meets the following criteria: - The elements are positive line 53 source
Source documentation
A set S belongs to Erdos939Sums r if it meets the following criteria:
- The elements are positive. 0 has no prime factors, so it is vacuously r-powerful, and the source means positive integers.
- The size of the set is $|S| = r - 2$ .
- The elements of the set are coprime (their greatest common divisor is 1).
- Every element in S is an $r$-powerful number.
- The sum of the elements in S, i.e., $\sum_{s \in S} s$ , is also an $r$-powerful number.
The summands are taken to be distinct (S is a Finset). The source does not say whether repeated summands are allowed; all known examples and constructions use distinct summands.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set, Finset
Proof uses: Set.ofPred, And, Eq, Finset.card, HSub.hSub, OfNat.ofNat, Finset.Coprime, Nat.Full, Finset.sum, Membership.mem, LT.lt
7 instances, coercions and auxiliary constants left out.
```
def Erdos939Sums (r : ℕ) :=
…
```
theorem Erdos939.erdos_939 If $r≥4$ then can the sum of $r-2$ coprime $r$-powerful numbers ever be itself $r$-powerful? sorry line 61 source
Source documentation
If $r≥4$ then can the sum of $r-2$ coprime $r$-powerful numbers ever be itself $r$-powerful?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Set.Nonempty, Finset, Erdos939.Erdos939Sums
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939 : answer(sorry) ↔ ∀ r ≥ 4, (Erdos939Sums r).Nonempty := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.finite If $r≥4$, are there at most finitely many sums of $r-2$ coprime $r$-powerful numbers that are themselves $r$-powerful? sorry line 77 source
Source documentation
If $r≥4$, are there at most finitely many sums of $r-2$ coprime $r$-powerful numbers that are themselves $r$-powerful?
The answer is no: for every $r \ge 6$ there are infinitely many such sums, see erdos_939.variants.infinite_of_six_le. (For $r = 4$ and $r = 5$ the question is open; for $r = 4$ no example is known at all, see erdos_939.) A construction in the site's comments, from GPT-5.5 Pro prompted by Price, gives infinitely many for every $r \ge 6$. This statement quantifies over every $r \ge 4$, so it stays open at $r = 4$ and $r = 5$. The category is unchanged because the construction is recorded in the comments and not in the literature.

depends on sorry what this means
Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, Set.Finite, Finset, Erdos939.Erdos939Sums
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.finite : answer(False) ↔ ∀ r ≥ 4, (Erdos939Sums r).Finite := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.infinite_of_six_le For every $r \ge 6$ there are infinitely many sums of $r - 2$ coprime $r$-powerful numbers that are themselves $r$-powerful sorry line 92 source
Source documentation
For every $r \ge 6$ there are infinitely many sums of $r - 2$ coprime $r$-powerful numbers that are themselves $r$-powerful.
A construction, found by GPT-5.5 Pro prompted by Liam Price and recorded in the comments on erdosproblems.com/939, expands $(X+Y)^r = (X-Y)^r + \sum_{j \text{ odd}} 2\binom{r}{j} X^{r-j} Y^j$, splits the $j = 3$ term into $\lfloor r/2 \rfloor - 2$ distinct pieces to obtain exactly $r - 2$ summands, and takes $X = q^r$, $Y = B^r$ with $B$ divisible by all primes in the coefficients and $q > B$ a prime not dividing $B$; varying $q$ gives infinitely many solutions.

L4DEL explanation
For every $r \ge 6$ there are infinitely many sums of $r - 2$ coprime $r$-powerful numbers that are themselves $r$-powerful. A construction, found by GPT-5.5 Pro prompted by Liam Price and recorded in the comments on erdosproblems.com/939, expands $(X+Y)^r = (X-Y)^r + \sum_{j \text{ odd}} 2\binom{r}{j} X^{r-j} Y^j$, splits the $j = 3$ term into $\lfloor r/2 \rfloor - 2$ distinct pieces to obtain exactly $r - 2$ summands, and takes $X = q^r$, $Y = B^r$ with $B$ divisible by all primes in the coefficients and $q > B$ a prime not dividing $B$; varying $q$ gives infinitely many solutions.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Set.Infinite, Finset, Erdos939.Erdos939Sums
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.infinite_of_six_le : ∀ r ≥ 6, (Erdos939Sums r).Infinite := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.triples Are there infinitely many triples of coprime $3$-powerful numbers $a, b, c$ such that $a + b = c$? sorry line 104 source
Source documentation
Are there infinitely many triples of coprime $3$-powerful numbers $a, b, c$ such that $a + b = c$?
The answer is yes. Nitaj [Ni95] proved it, with $2^3\cdot 3^5\cdot 73^3 + 271^3 = 919^3$ as an example. In Nitaj's construction at least two of $a, b, c$ are perfect cubes. Cohn [Co98] constructed infinitely many triples of which none is a perfect cube, and Walsh [Wa24] gave a further construction.

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Prod, Nat, Set.ofPred, Erdos939.erdos_939.variants.triples.match_1, And, Finset.Coprime, Insert.insert, Finset, Singleton.singleton, LT.lt, OfNat.ofNat, Nat.Full, Eq, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.triples :
    answer(True) ↔ {(a,b,c) | ({a, b, c} : Finset ℕ).Coprime ∧
      0 < a ∧ 0 < b ∧
      (3).Full a ∧ (3).Full b ∧ (3).Full c ∧
      a + b = c}.Infinite := by
…
```
Mentions: c
theorem Erdos939.erdos_939.variants.examples Cambie has found several examples of the sum of $r - 2$ coprime $r$-powerful numbers being itself $r$-powerful line 117 source
Source documentation
Cambie has found several examples of the sum of $r - 2$ coprime $r$-powerful numbers being itself $r$-powerful. For example when $r=5$ we have $$3^7\cdot 61^5 = 2^8\cdot3^{10}\cdot 5^7 + 2^{12}\cdot 23^6 + 11^5\cdot 13^5$$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, And, GE.ge, OfNat.ofNat, Set.Nonempty, Finset, Erdos939.Erdos939Sums
Proof uses: Exists.intro, Eq.mpr, id, Eq, Eq.trans, True, congrFun', congrArg, LE.le, eq_true_of_decide, Eq.refl, Bool, Bool.true, true_and, Set.ofPred, Finset.card, HSub.hSub, Finset.Coprime, Nat.Full, Finset.sum and 73 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.examples : (∃ r ≥ 4, (Erdos939Sums r).Nonempty) := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.seven Cambie has also found solutions when $r=7$ sorry line 132 source
Source documentation
Cambie has also found solutions when $r=7$.

depends on sorry what this means
Statement uses: Set.Nonempty, Finset, Nat, Erdos939.Erdos939Sums, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.seven : (Erdos939Sums 7).Nonempty := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.eight Cambie has also found solutions when $r=8$ sorry line 143 source
Source documentation
Cambie has also found solutions when $r=8$.
The source adds that the $r=8$ solution works "even with the sum of $5$ $8$-powerful numbers". That is a stronger result than this statement, which asks for the $r - 2 = 6$ summands of Erdos939Sums.

depends on sorry what this means
Statement uses: Set.Nonempty, Finset, Nat, Erdos939.Erdos939Sums, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.eight : (Erdos939Sums 8).Nonempty := by
…
```
Mentions: Erdos939.Erdos939Sums
theorem Erdos939.erdos_939.variants.euler Documented declaration: euler line 156 source
Source documentation
Euler had conjectured that the sum of $k - 1$ many $k$-th powers is never a $k$-th power, but this is false for $k=5$, as Lander and Parkin [LaPa67] found $$27^5+84^5+110^5+133^5=144^5$$.
The summands must be positive. Without that condition a set containing 0 would count, so the negation would be satisfied by a sum of fewer than $k-1$ powers and would claim less than the refutation of Euler's conjecture that this theorem records.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Nat, GE.ge, OfNat.ofNat, Finset, Eq, Finset.card, HSub.hSub, Membership.mem, LT.lt, Exists, Finset.sum, HPow.hPow
Proof uses: Eq.mpr, And, id, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Exists.intro, True, congr, eq_true, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natSub, true_and and 27 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_939.variants.euler : ¬ (∀ k ≥ 4, ∀ S : Finset ℕ, S.card = k - 1 →
    (∀ s ∈ S, 0 < s) → ¬ (∃ q, ∑ s ∈ S, s ^ k = q ^k)) := by
…
```