---

Claim. Google DeepMind's prover agent, in a Lean proof posted on 31 March 2026 by Moritz Firsching in the discussion thread of Problem 978, claims that the sextic

$$f(X)=X^6+33X^5+21X^4+63X^3+18X^2+24X+48$$

answers the second question no as it was then worded. The polynomial is irreducible by Eisenstein's criterion at $3$, has degree $6>3$, not a power of $2$, and a positive leading coefficient, and the post says that no $p^5$ divides all its values. But $f(X)\equiv X(X-1)\cdots(X-5)\pmod{16}$, and a product of six consecutive integers is divisible by $6!=720$, hence by $16$, so $2^4$ divides every $f(n)$ and no value is $4$-power-free. The post names formal-conjectures' statement erdos_978.parts.ii as the question proved false and gives the Lean proof in Firsching's fork of formal-conjectures, at the commit the link names. The erdosproblems.com wording then carried no local condition. The post's hypotheses include one at exponent $k-1$, no $p^5$ dividing every value, and formal-conjectures states the second question with that condition as its variant erdos_978.variants.allow_fixed_divisors, answered false.

Covers. The second question only, in its wording without the local condition at exponent $k-2$. The claim says nothing of the first and third questions.

Submission note. Posted to the erdosproblems.com forum by Moritz Firsching on 31 March 2026:

The DeepMind prover agent has formally verified that the answer to the second part of the question is 'False' by constructing an explicit counterexample polynomial (assuming our formalisation) of the question is correct).

The polynomial $f(X) = X^6 + 33X^5 + 21X^4 + 63X^3 + 18X^2 + 24X + 48$ satisfies all the hypotheses (irreducible, degree $> 3$, degree not a power of $2$, positive leading coefficient, no fixed $p^5$ divisor) yet $f(n)$ is never $4$-powerfree. Irreducibility follows from Eisenstein's criterion at $p = 3$, since $3$ divides all non-leading coefficients but $3^2 = 9 \nmid 48$, the constant coefficient. The key observation is that $f(X) \equiv X(X-1)(X-2)(X-3)(X-4)(X-5) \pmod{16}$, and the product of $6$ consecutive integers is always divisible by $6! = 720$, which is divisible by $16 = 2^4$. So $2^4 \mid f(n)$ for all $n$, meaning $f(n)$ is never $4$-powerfree - contradicting the conclusion that infinitely many values should be. The full formal proof in Lean 4 is available here).

Why it is rejected. It answers a variant, not the Statement. The second question of Problem 978, as the Statement asks it, assumes that for every prime $p$ some $n$ has $p^{k-2}\nmid f(n)$. The sextic fails that condition at $p=2$, since $2^4$ divides all its values, so it answers only the earlier wording without the condition at exponent $k-2$, which erdosproblems.com corrected the same day by adding it. The obstruction it exhibits is the local one that the condition excludes, so it settles no instance of the question as stated; its mathematics answers the variant and does not settle this problem. The value disproved is its answer to that variant.

Standing. Rejected, as answering a variant. The erdosproblems.com curator replied the same day that most papers on power-free values assume this local condition, that Erdős probably had it in mind, and that irreducible sextics failing it are known to people in the field, and added the condition to the statement. This corpus has not built the Lean proof, so it gives a formalization link and no formalized evidence.

Depends on. No page of this wiki.