Certifying non-existence of integer points on curves
Bogdan Grechuk, Eugene Go
math.GM
Oct 12, 2026 · v1
TL;DR
Insolubility proofs for 209 Diophantine equations, including large cubic-reciprocity certificates, are formalized in Lean 4, with Lean code partly generated by ChatGPT.
Abstract
We present an elementary but powerful method for proving that a two-variable equation has no integer solutions. The method produces quadratic identities which every integer solution must satisfy. Once these identities are established, a standard quadratic reciprocity argument finishes the proof. We illustrate the power of the method by resolving $25$ out of $30$ two-variable equations of size up to $34$ for which the problem of integer solubility remained open. We also resolve the remaining $5$ equations by deeper methods, and further determine the integer solubility of all two-variable equations of size up to $35$ and of length up to $12$, with two exceptions. Before this work, there were $211$ equations in this category that resisted the previously known methods, and we proved that $209$ of them have no integer solutions, with all proofs formalized in Lean. In addition, we show that our method can be used to solve certain two-variable equations whose integer solution set is non-empty.
Problem
For many small two-variable Diophantine equations, ordered by size or length, it was still unknown whether integer solutions exist. These are counterexamples to the integral Hasse principle that resisted known methods.
Approach
An elementary method derives quadratic identities H·T = U^2 + d·V^2 that every integer solution must satisfy, and then applies quadratic reciprocity via the Jacobi symbol to reach a contradiction. Equations the method cannot handle are treated with cubic (and quartic) reciprocity graphs over the Eisenstein (and Gaussian) integers. The resulting certificates, often too long for human checking, are formalized in Lean 4. The Lean code was largely produced by ChatGPT under guidance, and the authors checked the Lean statements.
Results
All 30 open equations of size up to 34 and 41 open equations of size 35 are resolved, completing integer solubility for all two-variable equations of size up to 35. All equations of length up to 12 are resolved except two. Of 211 previously resistant equations, 209 are proved to have no integer solutions, all with Lean formalizations in a public repository.
