GeoCoqInE-Tarski est un projet de démonstration et de vérification automatique de théorèmes géométriques. Il s'appuie sur le système de déduction Dedukti et le logiciel de preuve Coq. Il permet de formaliser des preuves géométriques et de les vérifier automatiquement, ce qui facilite la certification des résultats et la détection d'erreurs.