@misc{indiciae856b67dca659,
  title = {Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project},
  author = {Lawrence C Paulson},
  year = {2023},
  url = {https://arxiv.org/abs/2305.14407},
  note = {Source identifier: 2305.14407}
}