Bhavik Mehta and Jared Lichtman have launched a project to formalize in Lean a recent paper of Browning, Lichtman and Teräväinen on the number of exceptions to the abc conjecture: https://github.com/b-mehta/ABC-Exceptions . The methods are relatively elementary analytic number theory (relying heavily on geometry of numbers and Fourier analysis), but the computations are numerically tricky, which ought to be well suited for formal verification.