# Tag: HOL Light

- Porting the HOL Light metric space library (12 Jul 2023)

- The ALEXANDRIA Project: what has been accomplished? (27 Apr 2023)

- Porting libraries of mathematics between proof assistants (14 Sep 2022)

- Axiomatic type classes: some history, some examples (02 Mar 2022)

- ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician (08 Dec 2021)