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

github.com/Sobernard/Lindemann

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:

For the mathematical components library
For the mutivariate polynomial extension
For the Coquelicot library (you need version 2.1.2 of the coquelicot library, but the link given here may not be robust. Please perform an internet search in case of failure).
For a small library connecting the complex numbers of Coquelicot with the mathematical components framework

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

Improved version of the development on transcendance

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

LOCATION=/tmp/testLindemann

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 http://coq.inria.fr/opam/released
opam install coq.8.5.3 --yes

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

cd $LOCATION
wget https://github.com/ybertot/math-comp/archive/ITP-submission-version.tar.gz
tar xfz ITP-submission-version.tar.gz
mv math-comp-ITP-submission-version math-comp
wget https://www-sop.inria.fr/marelle/lindemann/multinomials.tar.gz
tar xfz multinomials.tar.gz
wget https://gforge.inria.fr/frs/download.php/file/36320/coquelicot-2.1.2.tar.gz
tar xfz coquelicot-2.1.2.tar.gz
wget https://www-sop.inria.fr/marelle/lindemann/Struct.tar.gz
tar xfz Struct.tar.gz
wget https://github.com/ybertot/Lindemann/archive/Modified-ITP-17-submission.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
./configure
./remake
./remake install

cd $LOCATION/multinomials
make
make install

cd ../Struct
coq_makefile -f _CoqProject > Makefile
make

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

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