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 + 2 b^2$.

翻译：我们用Coq 校对助理的数学组成部分图书馆撰写的Fermat两平方理论之和的两个正式证据作了评论。第一个证据是Zagier著名的一罪证;第二个证据是David Christopher最近依靠分区理论论点提出的证据。两个正式证据都依靠的是具有独立利益的有限系列演进的一般属性。证据技术大部分是通过特别战术自动执行经常性任务(如案件区分和自然数字的计算)。我们用同样方法,还提供了另一种形式证据,证明以美元2+2b2美元表格的质谱为主的经典结果。