Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
<|reference_start|>Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4: 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 of by Snyder in Lean 4, and also formalize many consequences of Mason-Stothers, including (i) non-solvability of Fermat-Cartan equations in polynomials, (ii) non-parametrizability of a certain elliptic curve, and (iii) Davenport's Theorem. We compare our work to existing formalizations of Mason-Stothers by Eberl in Isabelle and Wagemaker in Lean 3 respectively. Our formalization is based on the mathlib4 library of Lean 4, and is currently being ported back to mathlib4.<|reference_end|>
@article{baek2024formalizing,
    title={Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4},
    author={Jineon Baek, Seewoo Lee},
    journal={arXiv preprint arXiv:2408.15180},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.15180},
    primaryClass={cs.LO math.RA}
}