Erdős Problem #672

Erdős Problem 672 --- collection record

PROVENANCE AND STATUS

Saved collaborative-database status: verifiable. Snapshot checked: 2026-09-23T17:22:24Z. Latest status and formalization links: https://teorth.github.io/erdosproblems/

This is an attributed collection of existing writeups. The model-folder names below identify their original attribution; placement in GPT_6_Astra_Ultra does not attribute their mathematical work to that model. All locally available source versions selected for this problem are reproduced below, without editing their text.

Proof claims, computations, literature statements, and completion estimates in the reused text have not been independently verified in this collection pass. A source claiming a solution does not change the saved upstream status.

Primary source (latest numbered version in the preferred model folder): attacks/erdos/gpt_pro_5.2/672.tex.

REUSED SOURCE 1

1) FORMAL RESTATEMENT

Let $k\ge 4$ be an integer. Let $n,d\in\mathbb Z_{\ge 1}$ with $\gcd(n,d)=1$. Consider the arithmetic progression \[ n,\ n+d,\ \dots,\ n+(k-1)d \] of length $k$, and its product \[ P(n,d,k):=\prod_{i=0}^{k-1}(n+id)\in\mathbb Z_{\ge 1}. \] Question: Can $P(n,d,k)$ be a perfect power, i.e. can there exist integers $y\ge 1$ and $\ell\ge 2$ such that \[ P(n,d,k)=y^{\ell}? \]

2) QUICK LITERATURE/CONTEXT CHECK

As stated in the problem text: - Erdős--Selfridge $1975$ proved that the product of consecutive integers ($d=1$) is never a perfect power. - There are infinitely many $(n,d)$ with $\gcd(n,d)=1$ such that $n(n+d)(n+2d)$ is a square (Pell-equation phenomenon), so $k=3$ admits squares. - Results in the text rule out many cases, including impossibility for $4\le k\le 34$ (as quoted).

I do not use any other external results here.

3) ATTACK PLAN

Proof-oriented ideas: - Use gcd structure of terms in a primitive arithmetic progression ($\gcd(n,d)=1$) to control how primes can appear across different factors. - Use the constraint that primes $p>k-1$ can divide at most one term, forcing their exponents to be multiples of $\ell$ within a single term.

Disproof-oriented ideas: - Search for explicit counterexamples for small $k$ by brute force.

4) WORK

FAST REALITY CHECK (brute force)

I searched for solutions with $k\in\{4,5,6\}$, $1\le n\le 200$, $1\le d\le 50$, $\gcd(n,d)=1$, checking whether $\prod_{i=0}^{k-1}(n+id)$ is a perfect power (exponent $\ge2$). No solutions were found.

I extended the search for $k=4$ to $1\le n\le 1000$, $1\le d\le 200$ (still $\gcd(n,d)=1$), again finding no solutions.

Lemma 672.1 (primes dividing $d$ divide no term)

Assume $\gcd(n,d)=1$. Then for every integer $i\ge 0$, \[ \gcd(n+id,\ d)=1. \] In particular, if a prime $p$ divides $d$, then $p$ divides none of the terms $n+id$.

Proof. Using the Euclidean algorithm, \[ \gcd(n+id,d)=\gcd(n,d), \] because $\gcd(n+id,d)=\gcd(n+id-id,d)=\gcd(n,d)$. Since $\gcd(n,d)=1$, the claim follows.

Lemma 672.2 (large primes cannot hit two terms)

Assume $\gcd(n,d)=1$ and let $p$ be a prime. Suppose $p$ divides both $n+id$ and $n+jd$ for some integers $0\le i<j\le k-1$. Then $p\mid (j-i)$. In particular, if $p>k-1$ then $p$ divides at most one of the $k$ terms.

Proof. If $p\mid(n+id)$ and $p\mid(n+jd)$, then $p$ divides their difference \[ (n+jd)-(n+id)=(j-i)d. \] By Lemma 672.1, $\gcd(n+id,d)=1$, so no prime divisor of $n+id$ can divide $d$. In particular, $p\nmid d$. Since $p\mid (j-i)d$ and $p\nmid d$, we conclude $p\mid (j-i)$.

If $p>k-1$, then $1\le j-i\le k-1<p$, so $p\mid (j-i)$ is impossible unless $j-i=0$, contradicting $i<j$. Hence $p$ cannot divide two distinct terms.

Lemma 672.3 (prime-power exponent is localized for $p>k-1$)

Assume $\gcd(n,d)=1$ and suppose \[ \prod_{i=0}^{k-1}(n+id)=y^{\ell} \] for some integers $y\ge 1$ and $\ell\ge 2$. Let $p$ be a prime with $p>k-1$. Then there exists at most one index $i\in\{0,\dots,k-1\}$ with $p\mid(n+id)$, and if such $i$ exists then \[ v_p(n+id)\equiv 0\pmod{\ell}. \]

Proof. By Lemma 672.2, $p$ divides at most one term, so there is at most one such $i$. If $p$ divides $n+id$, then the exponent of $p$ in the product is exactly $v_p(n+id)$ (since no other factor contributes $p$). But the product equals $y^{\ell}$, so every prime exponent in it is a multiple of $\ell$. Hence $v_p(n+id)\equiv 0\pmod{\ell}$.

5) VERIFICATION

- Lemma 672.1: uses only $\gcd(n,d)=1$ and the identity $\gcd(n+id,d)=\gcd(n,d)$. - Lemma 672.2: the step "$p\nmid d$" uses Lemma 672.1 correctly. - Lemma 672.3: uses unique contribution of $p$ to the valuation when $p>k-1$.

Sanity check: if $d=1$ (consecutive integers) then Lemma 672.2 reduces to the familiar fact that a prime $p>k-1$ can divide at most one of $n,n+1,\dots,n+k-1$.

6) FINAL

UNRESOLVED

(i) Strongest proved partial result:

In a primitive progression ($\gcd(n,d)=1$), any prime $p>k-1$ divides at most one term, so in any hypothetical perfect-power identity $\prod_{i=0}^{k-1}(n+id)=y^{\ell}$, the $p$-adic valuation of that term must be a multiple of $\ell$.

(ii) First gap (crisp):

I cannot turn the localization of large prime powers (Lemma 672.3) into a contradiction for general $k\ge 4$.

(iii) Top 3 next moves:

1. Combine Lemma 672.3 with a lower bound guaranteeing existence of a prime $p>k-1$ dividing exactly one term to exponent $1$ (or to an exponent not divisible by $\ell$). This would require a "large prime factor" result for at least one term in the progression. 2. For fixed $k$, push computation further (larger $n,d$) and factor products to look for patterns in near-misses (e.g. products that are almost squares). 3. Investigate constraints coming from small primes $p\le k-1$ that can divide multiple terms; one would like to show they cannot supply the needed exponents to make all terms combine into an $\ell$th power.

(iv) Minimal counterexample structure:

A minimal counterexample would be a triple $(n,d,k)$ with $\gcd(n,d)=1$, $k\ge 4$, such that the product is an $\ell$th power with $\ell\ge 2$, and with all primes $p>k-1$ appearing only with exponents divisible by $\ell$ inside individual terms. One expects such a counterexample (if it exists) would force each term to be unusually "powerful" with respect to its large prime factors.

COMPLETION ESTIMATE

Newly verified progress in this collection pass: $0\%$. This measures new verification work, not the amount of mathematics achieved in the reused text.

OUTPUT

MODEL: Claude Opus 4.8 (agentic session in Claude Code; Lean 4 + Mathlib compile-verify loop) PROMPT STRATEGY: autonomous "prover loop" — multi-hour agentic session; every claimed step compiled with `lake env lean` against Mathlib and accepted only on exit 0; final theorems checked with `#print axioms`. Verification claims below are reported by the contributor; Lean proof artifacts are not included in this submission.

1) FORMAL RESTATEMENT Erdős Problem 672 (Euler's theorem, arithmetic core): for $n, d \ge 1$ with $\gcd(n,d)=1$, \[ n(n+d)(n+2d)(n+3d) \ne q^2 \quad \text{for all } q \in \mathbb{N}. \] (The product of a four-term arithmetic progression with coprime parameters is never a perfect square.) In Lean (matching the shape needed for the formal-conjectures statement $\mathrm{Erdos672With}\ 4\ 2$):

theorem euler_four_ap (n d : N) (hn : 0 < n) (hd : 0 < d)
    (hnd : n.Coprime d) (q : N) :
    n * (n + d) * (n + 2 * d) * (n + 3 * d) != q ^ 2

2) LITERATURE/CONTEXT CHECK Classical result of Euler $1780$. Modern reference used: Keith Conrad, "Arithmetic Progressions of Four Squares" and "Proofs by Descent" (UConn expository blurbs). Key facts from Conrad: (i) "no four rational squares in AP" is equivalent to the elliptic curve $y^2=x^3-x^2-4x+4$ (j-invariant $35152/9$) having rank 0; (ii) Fermat's $x^4-y^4\ne z^2$ is equivalent to rank 0 of the DIFFERENT curve $y^2=x^3-x$ $j = 1728$; (iii) Euler's elementary proof is an intricate descent on the pair $a^2+c^2=2b^2,\ b^2+d^2=2c^2$, which Conrad does not reproduce (he uses Kolyvagin/L-values). Mathlib has PythagoreanTriple.coprime_classification and not_fermat_42 ($a^4+b^4\ne c^2$) but NOT $x^4-y^4\ne z^2$, and no congruent-number/rank machinery.

3) ATTACK PLAN Backbone identities (all ring-verified): with $P=n(n+d)(n+2d)(n+3d)$, $A=n(n+3d)$, $B=(n+d)(n+2d)$, $X=n^2+3nd+d^2$: $P=AB$, $B=A+2d^2$, $P+d^4=X^2$. So $P=q^2$ makes $(q, d^2, X)$ a Pythagorean triple; prove it is primitive; classify; reduce each branch to a fourth-power Diophantine obstruction. Expected crux: Fermat-style descent for $x^4-y^4\ne z^2$ (not in Mathlib — must be built from scratch).

4) WORK (everything below is machine-verified Lean 4 unless marked as the open remainder) (a) CRUX PROVED FROM SCRATCH — Fermat's right-triangle theorem:

theorem no_fermat_sub : forall (a b c : Z),
    IsCoprime a b -> b != 0 -> c != 0 -> a^4 != b^4 + c^2

theorem triangular_not_fourth_power (m n : N)
    (h : m * (m + 1) = 2 * n ^ 4) : m = 0 \/ m = 1

5) VERIFICATION All completed theorems compile with `lake env lean` (exit 0, no errors) against Mathlib (toolchain lean4 v4.32.0-rc1), and `#print axioms` reports exactly [propext, Classical.choice, Quot.sound] — no sorry, no native_decide — for: no_fermat_sub, beven_factor, beven_step, triangular_not_fourth_power, Int.not_fermat_sub_coprime, Int.sq_ne_fourth_sub_fourth. The single remaining sorry is euler_four_ap itself (after the verified reduction). Machine verification replaces self-assessment: the gap is exactly delimited, not estimated.

6) FINAL STATUS: PARTIAL Problem 672 is NOT solved here. Proven and banked: Fermat's $x^4-y^4\ne z^2$ (new to the Lean ecosystem), the full structural reduction of Euler's statement to the four-squares-in-AP core, and the triangular-number corollary. Remaining: the four-squares-in-AP descent (Euler's pair-descent $a^2+c^2=2b^2$, $b^2+d^2=2c^2$, or elliptic-curve rank machinery), neither of which exists in Mathlib. All claims are machine-checked; the blocker is recorded, not papered over.

1) FORMAL RESTATEMENT

Let $k\ge 4$ be an integer. Let $n,d\in\mathbb Z_{\ge 1}$ with $\gcd(n,d)=1$. Consider the arithmetic progression \[ n,\ n+d,\ \dots,\ n+(k-1)d \] of length $k$, and its product \[ P(n,d,k):=\prod_{i=0}^{k-1}(n+id)\in\mathbb Z_{\ge 1}. \] Question: Can $P(n,d,k)$ be a perfect power, i.e. can there exist integers $y\ge 1$ and $\ell\ge 2$ such that \[ P(n,d,k)=y^{\ell}? \]

2) QUICK LITERATURE/CONTEXT CHECK

As stated in the problem text: - Erdős--Selfridge $1975$ proved that the product of consecutive integers ($d=1$) is never a perfect power. - There are infinitely many $(n,d)$ with $\gcd(n,d)=1$ such that $n(n+d)(n+2d)$ is a square (Pell-equation phenomenon), so $k=3$ admits squares. - Results in the text rule out many cases, including impossibility for $4\le k\le 34$ (as quoted).

I do not use any other external results here.

3) ATTACK PLAN

Proof-oriented ideas: - Use gcd structure of terms in a primitive arithmetic progression ($\gcd(n,d)=1$) to control how primes can appear across different factors. - Use the constraint that primes $p>k-1$ can divide at most one term, forcing their exponents to be multiples of $\ell$ within a single term.

Disproof-oriented ideas: - Search for explicit counterexamples for small $k$ by brute force.

4) WORK

FAST REALITY CHECK (brute force)

I searched for solutions with $k\in\{4,5,6\}$, $1\le n\le 200$, $1\le d\le 50$, $\gcd(n,d)=1$, checking whether $\prod_{i=0}^{k-1}(n+id)$ is a perfect power (exponent $\ge2$). No solutions were found.

I extended the search for $k=4$ to $1\le n\le 1000$, $1\le d\le 200$ (still $\gcd(n,d)=1$), again finding no solutions.

Lemma 672.1 (primes dividing $d$ divide no term)

Assume $\gcd(n,d)=1$. Then for every integer $i\ge 0$, \[ \gcd(n+id,\ d)=1. \] In particular, if a prime $p$ divides $d$, then $p$ divides none of the terms $n+id$.

Proof. Using the Euclidean algorithm, \[ \gcd(n+id,d)=\gcd(n,d), \] because $\gcd(n+id,d)=\gcd(n+id-id,d)=\gcd(n,d)$. Since $\gcd(n,d)=1$, the claim follows.

Lemma 672.2 (large primes cannot hit two terms)

Assume $\gcd(n,d)=1$ and let $p$ be a prime. Suppose $p$ divides both $n+id$ and $n+jd$ for some integers $0\le i<j\le k-1$. Then $p\mid (j-i)$. In particular, if $p>k-1$ then $p$ divides at most one of the $k$ terms.

Proof. If $p\mid(n+id)$ and $p\mid(n+jd)$, then $p$ divides their difference \[ (n+jd)-(n+id)=(j-i)d. \] By Lemma 672.1, $\gcd(n+id,d)=1$, so no prime divisor of $n+id$ can divide $d$. In particular, $p\nmid d$. Since $p\mid (j-i)d$ and $p\nmid d$, we conclude $p\mid (j-i)$.

If $p>k-1$, then $1\le j-i\le k-1<p$, so $p\mid (j-i)$ is impossible unless $j-i=0$, contradicting $i<j$. Hence $p$ cannot divide two distinct terms.

Lemma 672.3 (prime-power exponent is localized for $p>k-1$)

Assume $\gcd(n,d)=1$ and suppose \[ \prod_{i=0}^{k-1}(n+id)=y^{\ell} \] for some integers $y\ge 1$ and $\ell\ge 2$. Let $p$ be a prime with $p>k-1$. Then there exists at most one index $i\in\{0,\dots,k-1\}$ with $p\mid(n+id)$, and if such $i$ exists then \[ v_p(n+id)\equiv 0\pmod{\ell}. \]

Proof. By Lemma 672.2, $p$ divides at most one term, so there is at most one such $i$. If $p$ divides $n+id$, then the exponent of $p$ in the product is exactly $v_p(n+id)$ (since no other factor contributes $p$). But the product equals $y^{\ell}$, so every prime exponent in it is a multiple of $\ell$. Hence $v_p(n+id)\equiv 0\pmod{\ell}$.

5) VERIFICATION

- Lemma 672.1: uses only $\gcd(n,d)=1$ and the identity $\gcd(n+id,d)=\gcd(n,d)$. - Lemma 672.2: the step "$p\nmid d$" uses Lemma 672.1 correctly. - Lemma 672.3: uses unique contribution of $p$ to the valuation when $p>k-1$.

Sanity check: if $d=1$ (consecutive integers) then Lemma 672.2 reduces to the familiar fact that a prime $p>k-1$ can divide at most one of $n,n+1,\dots,n+k-1$.

6) FINAL

UNRESOLVED

(i) Strongest proved partial result:

In a primitive progression ($\gcd(n,d)=1$), any prime $p>k-1$ divides at most one term, so in any hypothetical perfect-power identity $\prod_{i=0}^{k-1}(n+id)=y^{\ell}$, the $p$-adic valuation of that term must be a multiple of $\ell$.

(ii) First gap (crisp):

I cannot turn the localization of large prime powers (Lemma 672.3) into a contradiction for general $k\ge 4$.

(iii) Top 3 next moves:

1. Combine Lemma 672.3 with a lower bound guaranteeing existence of a prime $p>k-1$ dividing exactly one term to exponent $1$ (or to an exponent not divisible by $\ell$). This would require a "large prime factor" result for at least one term in the progression. 2. For fixed $k$, push computation further (larger $n,d$) and factor products to look for patterns in near-misses (e.g. products that are almost squares). 3. Investigate constraints coming from small primes $p\le k-1$ that can divide multiple terms; one would like to show they cannot supply the needed exponents to make all terms combine into an $\ell$th power.

(iv) Minimal counterexample structure:

A minimal counterexample would be a triple $(n,d,k)$ with $\gcd(n,d)=1$, $k\ge 4$, such that the product is an $\ell$th power with $\ell\ge 2$, and with all primes $p>k-1$ appearing only with exponents divisible by $\ell$ inside individual terms. One expects such a counterexample (if it exists) would force each term to be unusually "powerful" with respect to its large prime factors.