Abstract:
Hilbert's concept of formal proof is an ideal of rigour for
mathematics which has important applications in mathematical logic,
but seems irrelevant for the practice of mathematics. The advent, in the
last twenty years, of proof assistants was followed by an impressive record
of deep mathematical theorems formally proved. Formal proof is practically
achievable. With formal proof, correctness reaches a standard that
no pen-and-paper proof can match, but an essential component of mathematics
- the insight and understanding - seems to be in short supply.
So, what makes a proof understandable? To answer this question we first
suggest a list of symptoms of understanding. We then propose a vision of
an environment in which users can write and check formal proofs as well
as query them with reference to the symptoms of understanding. In this
way, the environment reconciles the main features of proof: correctness
and understanding.
