# Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4

Preprint · Jineon Baek, Seewoo Lee

- Archive id: arxiv:2408.15180
- Published: 2024-08-27
- arXiv: https://arxiv.org/abs/2408.15180
- Source URL: https://arxiv.org/abs/2408.15180
- PDF: https://arxiv.org/pdf/2408.15180
- Provenance: arxiv

## 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 reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.