I am currently pursuing a PhD in computer science at Inria Sophia Antipolis in the MARELLE team, under the supervision of Yves Bertot and Laurence Rideau.

I work on the formalisation of mathematical theorems in the Coq proof-assistant, using the math-comp library.

# Lindemann-Weierstrass Theorem

This theorem gives a criterion to recognize transcendental numbers.

Coq statement :

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

Main mathematical formalization added :

- Multivariate polynomials which are symmetric on a subset of their indeterminates.
- Simple analysis for functions from R to C.
- Total order on the complex (not compatible with the multiplication), ...

The code is available on my Github repository and relies on coq 8.8.2 and math-comp 1.7.0.

The package (coq-lindemann) will soon be available through opam.