### 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.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Pi_Transcendental

- Pi_Transcendental_Polynomial_Library
- Pi_Transcendental

### Depends on

- The Transcendence of e
- Symmetric Polynomials

### Used by

- The Hermite–Lindemann–Weierstraß Transcendence Theorem

### Auto-related entries

- Hilbert’s Nullstellensatz
- Smooth Manifolds

## Cite

×

Pi_Transcendental-AFP

    @article{Pi_Transcendental-AFP,
      author  = {Manuel Eberl},
      title   = {The Transcendence of π},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Pi_Transcendental.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Oct 2, 2018 : Isabelle2018