Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples

 

Title:	Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
Author:	Roelof Oosterhuis
Submission date:	2007-08-12
Abstract:	This document presents the mechanised proofs of Fermat's Last Theorem for exponents 3 and 4 and the parametrisation of Pythagorean Triples.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Fermat3_4-2009-04-29.tar.gz Isabelle 2008: afp-Fermat3_4-2008-06-10.tar.gz Isabelle 2007: afp-Fermat3_4-2007-11-27.tar.gz