**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

This entry shows the transcendence of π based on the
classic proof using the fundamental theorem of symmetric polynomials
first given by von Lindemann in 1882, but the formalisation mostly
follows the version by Niven. The proof reuses much of the machinery
developed in the AFP entry on the transcendence of
*e*.