[Allan]

In order to be a mathematician it is necessary
though not sufficient
to suffer from a psychological disorder
which results in a total inability to communicate with normal human beings
in words they can understand.

[Mitchell]

I thought this article made sense :-).

But it's not about a deep question of mathematical philosophy, it's about a practical question. How can mathematical proofs be conveyed in a way that the details can be checked? Or maybe: how can mathematical proofs be written in a way that the details can be checked by an automated proof checker?

By the way, Devlin is a well-known set theorist. He also has an extinct opossum named after him.