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.