Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant
Clinical Orthopaedics and Related Research(2005)
摘要
We present the proof of Diophantus' 20th problem (book VI of Diophantus'
Arithmetica), which consists in wondering if there exist right triangles whose
sides may be measured as integers and whose surface may be a square. This
problem was negatively solved by Fermat in the 17th century, who used the
"wonderful" method (ipse dixit Fermat) of infinite descent. This method, which
is, historically, the first use of induction, consists in producing smaller and
smaller non-negative integer solutions assuming that one exists; this naturally
leads to a reductio ad absurdum reasoning because we are bounded by zero. We
describe the formalization of this proof which has been carried out in the Coq
proof assistant. Moreover, as a direct and no less historical application, we
also provide the proof (by Fermat) of Fermat's last theorem for n=4, as well as
the corresponding formalization made in Coq.
更多查看译文
关键词
number theory,software engineering
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要