The generalized Fermat equation x² + y⁵ = z⁷
A Lean 4 and Mathlib formalization of the main results of the paper "The generalized Fermat equation x² + y⁵ = z⁷" by Manvir Jaswal. Following Putz, a solution is a triple of integers (X, Y, Z) with X⁵ + Y² = Z⁷, gcd(X, Y, Z) = 1 and XYZ ≠ 0; put η = X⁵/Z⁷ and A_η = ℚ[t]/(f_η), where f_η(t) = 4t⁵ψ(t) − η(4t − 1) and ψ(t) = 25t³ + 20t² + 14t + 14. Theorem 1.1 says that A_η is never isomorphic to Putz's octic field L₈ = ℚ[x]/(h), where h(x) = x⁸ + 4x⁷ − 28x⁶ − 168x⁵ − 140x⁴ + 560x³ + 840x² − 480x − 940. Theorem 1.2 combines this with Putz's Theorem 4.33, which says that A_η is always…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-09-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-09-000002/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-10-09-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'