{"id":"palomar/PALOMAR-2026-08-27-000010","url":"https://github.com/BrandonMYates/yz-cubic-comparator/tree/70082c378b76b2eb9cec74de67506d1c0e36a514","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000010-v1.json","repo":"https://github.com/BrandonMYates/yz-cubic-comparator","tags":["math.NT","math.AC","msc:11D25","msc:12E05","msc:13P15","number-theory","lean","diophantine-equations","polynomial-parametrization"],"score":0,"title":"BrandonMYates/yz-cubic-comparator","trust":"high","domain":"math.NT","source":"palomar","authors":["Brandon Yates"],"reviews":0,"subject":"math.NT","summary":"This project formalizes in Lean 4 the statement that the Diophantine equation y*z*(y+z) = x^3 + x^2 + 3x - 1 admits no polynomial parametrization over the rationals whose x-coordinate has degree between 1 and 4. Writing f = X^3 + X^2 + 3X - 1, the compared theorem is that there is no triple of rational polynomials (g, u, v) with g nonconstant of degree at most 4 satisfying the identity u*v*(u+v) = f composed with g. Exhibiting such a family is one of the two standard ways an equation of this shape is settled affirmatively -- the other being a sporadic solution -- and the theorem closes that…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true}