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
highschool student. In short, the statement of the
theorem is that three nonzero 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,
A^{n} +
B^{n} +
C^{n} = 0 implies
n ≤ 2 for coprime polynomials
A, B, C
over a field. 
BibTeX: 
@article{Mason_StothersAFP,
author = {Manuel Eberl},
title = {The Mason–Stothers Theorem},
journal = {Archive of Formal Proofs},
month = dec,
year = 2017,
note = {\url{https://isaafp.org/entries/Mason_Stothers.html},
Formal proof development},
ISSN = {2150914x},
}
