On the polynomial values represented by binary quadratic forms

Abstract

Many Diophantine equations can be reduced to the question of whether, for a given non-degenerate integral binary quadratic form $F$ and a univariate polynomial $P$ with integer coefficients, $P(x)$ can be represented by $F$ for infinitely many values of $x$. We develop a method for answering this question for certain cubic and quartic polynomials $P$, as well as for certain polynomials of the form $P(x)=R(Q(x))$, where $R(t)$ and $Q(x)$ are polynomials of degrees $3$ and $2$, respectively. Applying this method with $F(y,z)=y^2+z^2$, $R(t)=t^3-4$ and $Q(x)=x^2$, we conclude that $x^6-4$ is a sum of two squares infinitely often. In turn, this implies that the equation $y^2+x^3y+z^2+1=0$ has infinitely many integer solutions. Prior to this work, it was the shortest equation for which it was unknown whether its integer solution set is finite or infinite. We conclude with a list of the new shortest equations for which the finiteness problem remains open. All main results of this paper have been formalized in Lean using Aristotle.