### Abstract

This article provides a formalisation of Snyder’s simple and elegant proof of the Mason–Stothers theorem, which is the polynomial analogue of the famous abc Conjecture for integers. Remarkably, Snyder found this very elegant proof when he was still a high-school student.

In short, the statement of the theorem is that three non-zero coprime polynomials A, B, C over a field which sum to 0 and do not all have vanishing derivatives fulfil max{deg(A), deg(B), deg(C)} < deg(rad(ABC)) where the rad(P) denotes the radical of P, i. e. the product of all unique irreducible factors of P.

This theorem also implies a kind of polynomial analogue of Fermat’s Last Theorem for polynomials: except for trivial cases, An + Bn + Cn = 0 implies n ≤ 2 for coprime polynomials A, B, C over a field.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Mason_Stothers

- Mason_Stothers

### Used by

- Elimination of Repeated Factors Algorithm

## Cite

×

Mason_Stothers-AFP

    @article{Mason_Stothers-AFP,
      author  = {Manuel Eberl},
      title   = {The Mason–Stothers Theorem},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Mason_Stothers.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Dec 22, 2017 : Isabelle2017