Formalisation vs. Understanding A Case Study in Isabelle

摘要

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