Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4

TL;DR

This paper formalizes the Mason-Stothers Theorem and its corollaries in Lean 4, providing a foundation for further formal proofs in number theory related to the ABC conjecture and Fermat's Last Theorem.

Contribution

It presents the first formalization of an elementary proof of Mason-Stothers Theorem in Lean 4, including key consequences and comparison with prior formalizations.

Findings

Formalized Mason-Stothers Theorem in Lean 4.

Proved several corollaries including Fermat-Cartan equations and Davenport's Theorem.

Integrated formalization into Lean 4's mathlib library.

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.