TY - RPRT TI - Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project AU - Lawrence C Paulson PY - 2023 UR - https://arxiv.org/abs/2305.14407 ID - 2305.14407 ER -