Formal verification of Zagier's one-sentence proof
Dubach, Guillaume
Mühlböck, Fabian
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 recent new 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.
2021
info:eu-repo/semantics/preprint
doc-type:preprint
text
http://purl.org/coar/resource_type/c_816b
https://research-explorer.ista.ac.at/record/9281
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>. doi:<a href="https://doi.org/10.48550/arXiv.2103.11389">10.48550/arXiv.2103.11389</a>
eng
info:eu-repo/semantics/altIdentifier/doi/10.48550/arXiv.2103.11389
info:eu-repo/semantics/altIdentifier/arxiv/2103.11389
info:eu-repo/grantAgreement/EC/H2020/754411
info:eu-repo/semantics/openAccess