On the polynomial values represented by binary quadratic forms

Many Diophantine equations can be reduced to the question of whether, for a given non-degenerate integral binary quadratic form [Formula: see text] and a univariate polynomial [Formula: see text] with integer coefficients, [Formula: see text] can be represented by [Formula: see text] for infinitely many values of [Formula: see text]. We develop a method for answering this question for certain cubic and quartic polynomials [Formula: see text], as well as for certain polynomials of the form [Formula: see text], where [Formula: see text] and [Formula: see text] are polynomials of degrees [Formula: see text] and [Formula: see text], respectively. Applying this method with [Formula: see text], [Formula: see text] and [Formula: see text], we conclude that [Formula: see text] is a sum of two squares infinitely often. In turn, this implies that the equation [Formula: see text] 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.