These links are intended to put HLM into context, but are not meant to be an exhaustive list or categorization. Items in italics refer to projects that do not focus on formally verified abstract mathematics, but where I somehow felt the list would be incomplete without them. Browse the external link collections at the bottom for further reading.

In contrast to HLM, a few proof assistants are already quite mature, and have been used to formalize a significant amount of mathematics:

- Based on set theory:
- Based on type theory:
- Based on typed higher order logic:

- Mathematical libraries of/for proof assistants:
- Mizar Mathematical Library and Formalized Mathematics journal
- Mathematical library of HOL Light
- The Archive of Formal Proofs for Isabelle
- IsarMathLib for Isabelle/ZF (See also Slawomir Kolodynski's blog.)
- Coq contribs
- C-CoRN for Coq
- Metamath

- Large proofs:
- Prime number theorem, by Jeremy Avigad
- Four-color theorem, by Georges Gonthier
- Jordan curve theorem, by Thomas Hales
- Flyspeck, a long-term project led by Thomas Hales to formalize his proof of the Kepler conjecture

- Mathematical knowledge management:
- Status reports:
- Freek Wiedijk's list tracking the progress of formalizing 100 theorems in different proof assistants
- Notices of the AMS: A Special Issue on Formal Proof
- Freek Wiedijk: The Seventeen Provers of the World

Please let me know if a link is broken or if you think something is missing.