Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827)

The main goal of the paper is to give an overview of the author's work experiences with Isabelle/HOL so far and of the author's views on the formalisation of mathematics, and to share some instructions on getting started with Isabelle as well as some first observations which the author made, both technical and conceptual ones, that might prove to be helpful to students and beginners in their early learning stages. In particular, the author introduced the ALEXANDRIA project at the University of Cambridge.