Galapagos is an ANR-funded project on proofs in geometry, both concerning elementary geometry and algorithmic geometry
Formath is an EU STREP FET-open project lead by Thierry Coquand at Gothenburg University. It is concerned with the formalisation of mathematics