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.