---
res:
bibo_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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Guillaume
foaf_name: Dubach, Guillaume
foaf_surname: Dubach
foaf_workInfoHomepage: http://www.librecat.org/personId=D5C6A458-10C4-11EA-ABF4-A4B43DDC885E
orcid: 0000-0001-6892-8137
- foaf_Person:
foaf_givenName: Fabian
foaf_name: Mühlböck, Fabian
foaf_surname: Mühlböck
foaf_workInfoHomepage: http://www.librecat.org/personId=6395C5F6-89DF-11E9-9C97-6BDFE5697425
orcid: 0000-0003-1548-0177
bibo_doi: 10.48550/arXiv.2103.11389
dct_date: 2021^xs_gYear
dct_language: eng
dct_title: Formal verification of Zagier's one-sentence proof@
...