BrandonMYates/yz-cubic-comparator
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-27-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'