Formal verification of Zagier's one-sentence proof. - Guillaume Dubach; Fabian Muehlboeck (CoRR, 2021)