preprint
Formal verification of Zagier's one-sentence proof
draft
Guillaume
Dubach
author D5C6A458-10C4-11EA-ABF4-A4B43DDC885E0000-0001-6892-8137
Fabian
Mühlböck
author 6395C5F6-89DF-11E9-9C97-6BDFE56974250000-0003-1548-0177
LaEr
department
ToHe
department
ISTplus - Postdoctoral Fellowships
project
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
eng
arXiv
2103.11389
https://research-explorer.app.ist.ac.at/record/9946
Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, n.d.
G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” <i>arXiv</i>. .
G. Dubach, F. Mühlböck, ArXiv (n.d.).
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>.
Dubach, G., & Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence proof. <i>arXiv</i>.
Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” <i>ArXiv</i>, 2103.11389.
Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389.
92812021-03-23T05:38:48Z2021-10-08T10:05:46Z