### 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,
*A ^{n}* +

*B*+

^{n}*C*= 0 implies n ≤ 2 for coprime polynomials

^{n}*A*,

*B*,

*C*over a field.