Groups

• The Calculemus Project
• Computer Algebra and Automated Reasoning (CAAR) Group at St. Andrews
• Atypical: Integrating Computer Algebra and Reasoning
• Mathematical Knowledge Management (MKM)
• The Theorema Project

Systems

• Coq
• Isabelle
• Agda
• PVS
• ACL2
• matita
• NuPRL
• MIZAR
• IMPS Interactive Mathematical Proof System

and a whole lot more.