Abstract
This document presents the mechanised proofs of
BSD License- Fermat's Last Theorem for exponents 3 and 4 and
- the parametrisation of Pythagorean Triples.