[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.

[Allan]

The article is somewhat interesting
but this 'left-wing' 'right-wing' business is idiotic.
He's trying to be cute but it makes him look like an idiot.
Mathematicians shouldn't attempt humour or wit
they are not good at it
because they are essentially humourless.