Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4

Abstract

The ABC conjecture implies many conjectures and theorems in number theory, including the celebrated Fermat's Last Theorem. Mason-Stothers Theorem is a function field analogue of the ABC conjecture that admits a much more elementary proof with many interesting consequences, including a polynomial version of Fermat's Last Theorem. While years of dedicated effort are expected for a full formalization of Fermat's Last Theorem, the simple proof of Mason-Stothers Theorem and its corollaries calls for an immediate formalization. We formalize an elementary proof by Snyder in Lean 4, and also formalize many consequences of Mason-Stothers, including nonsolvability of Fermat-Cartan equations in polynomials, nonparametrizability of a certain elliptic curve, and Davenport's Theorem. We compare our work to existing formalizations of the Mason-Stothers by Eberl in Isabelle and Wagemaker in Lean 3 respectively. Our formalization has been integrated into the mathlib library of Lean 4.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.