Also see this: http://www.michaelbeeson.com/research/CheckEuclid/index.php http://www.michaelbeeson.com/research/CheckEuclid/index.php It seems a dependently t

Also see this: http://www.michaelbeeson.com/research/CheckEuclid/index.php http://www.michaelbeeson.com/research/CheckEuclid/index.php It seems a dependently typed language might be overkill, "The proofs described in this paper only need a rather weak logic. There are no function symbols", "only existential quantifiers; universal quantification over the free variables is left implicit." They wrote a translator then to convert the proofs to HOL, and Coq, you could presumably do the same for e.g. idris