Get HLM at Fast, secure and Free Open Source software downloads

The HLM Proof Assistant

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.

Proof Assistants

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

Formalized Mathematics

Link Collections

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