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:
Please let me know if a link is broken or if you think something is missing.