Department of Mathematics FAS Harvard University One Oxford Street Cambridge MA 02138 USA Tel: (617) 495-2171 Fax: (617) 495-5132
FAS Computer Services to Harvard University IT: (617) 495-7777.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Download page:

An example from the documentation:

Fixpoint gcd a b :=
  match a with
   | O => b
   | S a' => gcd (b mod (S a')) (S a')

Definition divide x y := exists z, y=z*x.
Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.

Lemma gcd_divide   : forall a b, (gcd a b | a) / (gcd a b | b).
Lemma gcd_divide_l : forall a b, (gcd a b | a).
Lemma gcd_divide_r : forall a b, (gcd a b | b).
Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).

Simplicity, Clarity, Generality B.W. Kernighan, R. Pike, in "The Practice of Programming".