At first, the (sequence of) Fermat numbers (the -th Fermat
number is denoted as ) is defined, see df-fmtno, and
basic theorems are provided. Afterwards, it is shown that the first five
Fermat numbers are prime, the (first) five Fermat primes, see
fmtnofz04prm, but that the fifth Fermat number (counting starts at !)
is not prime, see fmtno5nprm. The fourth Fermat number (i.e., the fifth
Fermat prime) is currently the
biggest number proven to be prime in set.mm, see 65537prm (previously, it
was , see 4001prm).
Another important result of this section is Goldbach's theorem goldbachth,
showing that two different Fermut numbers are coprime. By this, it can be
proven that there is an infinite number of primes, see prminf2.
Finally, it is shown that every prime of the form must
be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno.