Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant

David Delahaye, Micaela Mayero

We present the proof of Diophantus' 20th problem (book VI of Diophantus' Arithmetica), which consists in wondering if there exist right triangles whose sides may be measured as int…