# 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


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