Formal verification of Zagier's one-sentence proof

arXiv2103.11389MaRDI QIDQ6363357

Author name not available (Why is that?)

Publication date: 21 March 2021

Abstract: We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's more recent proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics. With the same method, we also provide a formal proof of another classical result on primes of the form $a^2+2b^2$.

Has companion code repository: https://github.com/gdubach/Zagier_project

Mathematics Subject Classification ID

No records found.

This page was built for publication: Formal verification of Zagier's one-sentence proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6363357)