IsTranscendentalPi

This repository contains a Lean 4 formalization of the transcendence of , which appears as Theorem 53 on Freek Wiedijk’s list of 100 classic theorems for proof assistants; see Freek Wiedijk’s list for progress across multiple theorem provers, and the Lean 100 page, which tracks the status of these theorems specifically in Lean/mathlib.

The transcendence of was first proved by Lindemann in 1882 ¹ as a corollary of the more general Lindemann-Weierstrass theorem, which states that if are algebraic numbers linearly independent over , then are algebraically independent. On Freek Wiedijk's list, this result appears as Theorem 54. There is also ongoing work to formalize the Lindemann-Weierstrass theorem in mathlib; see Astrainfinita's mathlib4 fork, in particular the transcendental branch, as well as the current Mathlib/NumberTheory/Transcendental/Lindemann development in the main mathlib4 repository.

It is, however, also possible to give a direct proof of the transcendence of without using the Lindemann-Weierstrass theorem; this repository presents the self-contained and elegant proof given by Niven in 1939 ². This project also benefited from the Coq formalization of the same proof by Bernard, Bertot, Rideau, and Strub ³, as well as from Eberl's Isabelle formalization ⁴.

Project history

This project began as James Huang's final project for the master's course Formalising Mathematics in the 2023-2024 academic year, taught by Prof Kevin Buzzard; see the Formalising Mathematics course notes. The original goal proved too ambitious for the course project alone, but after the end of the course James Huang and Samuël Borza teamed up to rework and complete the formalization. The present repository is the result of this collaboration.

Sketch of the proof

We argue by contradiction, assuming that is algebraic. Then is algebraic as well, so there exists a monic polynomial such that

By the fundamental theorem of algebra, we may write

where are the roots of , one of which is . Since by Euler's identity, one obtains

and, after expanding this product, one gets

Equivalently,

where

The next step is to package these numbers as the roots of a new polynomial , so that

By Vieta's formulas, the -th coefficient of is

where denotes the -th elementary symmetric polynomial. Note that this coefficient can also be obtained by evaluating the multivariate polynomial

at , where

The polynomial being symmetric, the fundamental theorem of symmetric polynomials implies that can be expressed as a polynomial in the elementary symmetric polynomials

Evaluating at , it follows that can be expressed in terms of the elementary symmetric polynomials in the roots of , and hence, by Vieta's formulas, in terms of the coefficients of . Therefore, . By clearing denominators, one obtains an integer polynomial and a nonzero integer such that .

Following Niven, the proof then introduces the auxiliary polynomial

An integration-by-parts and the previous identity then shows that

where

Since , one has for some , and thus .

By bounding uniformly for , and then using to control the integrand, it follows that for all sufficiently large ,

A contradiction would follow from showing that . Indeed, in that case the quantity

is also an integer, and in fact a nonzero integer for all sufficiently large prime numbers . If it were zero, then would divide , and hence would divide . But is a fixed integer, so it can be divisible by only finitely many primes. Therefore, for all sufficiently large prime numbers , one has

contradicting the previous bound.

It remains to show that . We write

and introduce the polynomial

The polynomial is chosen specifically so that

Furthermore, the numbers are the roots of the monic polynomial

where .

The polynomial is clearly symmetric. By the fundamental theorem of symmetric polynomials once again, it can therefore be expressed as a polynomial in the elementary symmetric polynomials in . Since are the roots of the monic polynomial with integer coefficients introduced above, it follows that is an integer.

Therefore, we conclude that

and the proof is complete.

File structure

We briefly explain the role of each file, following the order in which the argument is assembled in the proof.

• IsTranscendentalPi/IncrementalDerivatives.lean:

  Develops the basic differential identities for functions of the form and . These lemmas are used to differentiate the expressions that later appear in and in the repeated integration-by-parts argument.

• IsTranscendentalPi/SymmetricPolynomials.lean:

  Contains the symmetric-polynomial machinery used throughout the construction of . In particular, it shows how symmetric expressions in roots can be rewritten in terms of polynomial coefficients via the elementary symmetric polynomials and Vieta's formulas.

• IsTranscendentalPi/ComplexExponential.lean:

  Proves the combinatorial-exponential identities coming from . It defines subset sums and nonzero subset sums, and derives the relation from the root condition .

• IsTranscendentalPi/CalculusOnPoly.lean:

  Introduces the integral and proves the basic integration-by-parts identity that rewrites it in terms of sums of derivatives of . This is the calculus core that later gets specialized to the auxiliary polynomials .

• IsTranscendentalPi/NivenPolynomials.lean:

  Introduces Niven's auxiliary polynomials , , and , and proves their fundamental algebraic properties. In particular, it relates to the higher derivatives of and computes the contribution of roots and root multiplicities to the sums appearing in the main identity.

• IsTranscendentalPi/SubsetSumPolynomial.lean:

  Constructs the polynomial whose roots are the nonzero subset sums of the roots of . It also proves that , clears denominators to obtain , and studies the monic rescaling whose roots are .

• IsTranscendentalPi/ScaledAuxiliaryPolynomial.lean:

  Proves the integrality statement for the scaled sums involving . It introduces the symmetric polynomials and shows that evaluating them at yields the terms , from which one deduces .

• IsTranscendentalPi/AnalyticEstimates.lean:

  Establishes the analytic upper and lower bounds that drive the contradiction. On the one hand, it shows that the scaled integral expression is eventually smaller than ; on the other hand, it rewrites the same expression as times a nonzero integer for sufficiently large primes.

• IsTranscendentalPi/Main.lean:

  Assembles the previous ingredients into the final contradiction argument. Starting from the assumption that is algebraic, it constructs the polynomial , the nonzero subset sums , the auxiliary polynomial , and finally combines the analytic and arithmetic estimates to prove that is transcendental.

Build and Dependencies

This project uses:

• Lean 4
• mathlib

The exact toolchain is pinned in lean-toolchain. To build the project, run

lake build

Authors, License, and Final Comments

James Huang and Samuël Borza.

This project is released under the Apache 2.0 license, matching mathlib's license; see LICENSE.

Comments, corrections, improvements, and pull requests are very welcome!

References

Footnotes

1. Ferdinand von Lindemann, Über die Ludolph'sche Zahl, Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften zu Berlin, vol. 2 (1882), pp. 679–682; and Über die Zahl π, Mathematische Annalen 20(2) (1882), pp. 213–225. ↩

2. Ivan Niven, "The transcendence of pi," American Mathematical Monthly 46(8) (1939), pp. 469–471. ↩

3. Sylvie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub, "Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials," in Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (2016), pp. 76–87. ↩

4. Manuel Eberl, "The Transcendence of π," Archive of Formal Proofs (September 2018), https://isa-afp.org/entries/Pi_Transcendental.html. ↩