Formal proof of the Lindemann-Weierstrass theorem

This page contains links to the Coq sources for the formalization of the Lindemann-Weierstrass theorem on transcendance. The author of this proof is Sophie Bernard.

The formalized theorem statement

The main statement of the formal proof is as follows:

Theorem LindemannWeierstrass n (alpha : complexR ^ n) :
  (n > 0)%N -> (forall i : 'I_n, alpha i is_algebraic) ->
  lin_indep_over Cint alpha -> alg_indep_over Cint (finfun (Cexp \o alpha)).

This reads as follows: for every n and every n numbers αi (0 ≤ i < n), if all the αi are algebraic complex numbers, and if the αi are rationally independent, then the numbers eαi are algebraically independent. To be more precise, the definitions of rationally independent and algebraically independent are given as follows:

Definition lin_indep_over (P : pred_class) {n : nat} (x : complexR ^ n) :=
  forall (lambda : complexR ^ n), lambda \in ffun_on P ->
    lambda != 0 -> \sum_(i < n) (lambda i * x i) != 0.

Definition alg_indep_over (P : pred_class) {n : nat} (x : complexR ^ n) :=
  forall (p : {mpoly complexR[n]}), p \is a mpolyOver _ P ->
    p != 0 -> p.@[x] != 0.

The notations in these statements are mostly borrowed from the mathematical components library.

The Hermite-Lindemann theorem

As a corollary, we proved the Hermite-Lindemann theorem which is stated as follows:

Theorem HermiteLindemann (x : complexR) :
  x != 0 -> x is_algebraic -> ~ ((Cexp x) is_algebraic).

The full development and its evolution

Sources of the coq code can be gathered from the following git repository

This code depends on libraries that are not distributed with Coq, and in particular on our own modified version of the mathematical components library. These libraries are available at the following addresses:

Synchronized version with submitted articles

article "Formalization of the Lindemann-Weierstrass Theorem"

We submitted a paper "Formalization of the Lindemann-Weierstrass Theorem" to the conference Interactive Theorem Proving in 2017. The versions at the time of submission are here:

After a few days of testing, we finally fixed the development as follows (modification are only in the way libraries are connected together).

In these files, the statement of the theorem is as follows

Theorem Lindemann n (alpha : complexR ^ n) :
  (n > 0)%N -> (forall i : 'I_n, alpha i is_algebraic) ->
  (forall (lambda : complexR ^ n), (forall i : 'I_n, lambda i \is a Cint) ->
    (exists i : 'I_n, lambda i != 0) -> \sum_(i < n) (lambda i * alpha i) != 0) ->
  forall P, P \is a mpolyOver _ Cint -> P != 0 -> P.@[finfun (Cexp \o alpha)] != 0.

Proposed process for compiling the files

Install opam version 1.2.2, for instance by using the following command on recent versions of Debian or Ubuntu.

apt-get install opam

or the following command on recent version of fedora

dnf install opam

You can then install a temporary version of Coq 8.5.3 by applying the following commands


mkdir -p $LOCATION
opam init --root=$LOCATION/opam --no-setup  --comp=4.02.3
eval $(opam config env --root=$LOCATION/opam)
opam switch 4.02.3
eval $(opam config env --root=$LOCATION/opam)
opam repo add coq-released
opam install coq.8.5.3 --yes

The next stage is to download all the sources for this development.

tar xfz ITP-submission-version.tar.gz
mv math-comp-ITP-submission-version math-comp
tar xfz multinomials.tar.gz
tar xfz coquelicot-2.1.2.tar.gz
tar xfz Struct.tar.gz
tar xfz Modified-ITP-17-submission.tar.gz
mv Lindemann-Modified-ITP-17-submission Lindemann

You can then start compiling the various libraries. This was tested on a machine runnning Fedora 25.

cd $LOCATION/math-comp/mathcomp
make ssreflect/all_ssreflect.vo algebra/all_algebra.vo real_closed/bigenough.vo field/algC.vo
make real_closed/complex.vo
make install

cd $LOCATION/coquelicot-2.1.2
./remake install

cd $LOCATION/multinomials
make install

cd ../Struct
coq_makefile -f _CoqProject > Makefile

cd ../Lindemann
coq_makefile -f _CoqProject -o Makefile

You can then run Coq and load the final theorems by typing the following instructions

cd $LOCATION/Lindemann
coqtop -R ../Struct structs -R . Lind

(* at the Coq prompt. *)
From mathcomp Require Import all_ssreflect all_algebra.
From structs Require Import Rstruct Cstruct.

From SsrMultinomials Require Import mpoly.

Import ArchimedeanTheory.

Require Import seq_Lind.

About Lindemann.

Maintained by Yves Bertot. This page was modified on June 28th, 2017