Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
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 …