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

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.

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

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:

- 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

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.

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*