Formal verification of Zagier's one-sentence proof
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.
Download (ext.)
Preprint
| Submitted
| English
Corresponding author has ISTA affiliation
Department
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 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.
Publishing Year
Date Published
2021-03-21
Journal Title
arXiv
Article Number
2103.11389
IST-REx-ID
Cite this
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv. doi:10.48550/arXiv.2103.11389
Dubach, G., & Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence proof. arXiv. https://doi.org/10.48550/arXiv.2103.11389
Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2103.11389.
G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” arXiv. .
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.
Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” ArXiv, 2103.11389, doi:10.48550/arXiv.2103.11389.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)
Access Level
Open Access
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2103.11389
Google Scholar