We discuss how formalisation using proof assistants, an unconventional way of doing mathematics which seems to disregard Gödel’s celebrated Incompleteness Theorems, interacts with ideas of understanding. Our experience is based on a formalisation carried out in the Isabelle generic proof assistant.