Theorems need folk

Brian Davies's admission that mathematicians may in future have to rely on computers to check some theorems makes you wonder how those mathematicians can be sure they have set up their computers properly to produce correct results that humans cannot verify (Opinion, September 1).

As Brian Davies says, "pure mathematicians still have to devise the strategies that computers follow".

This was the very topic of an article of mine in Philosophy Now a few years ago. I was prompted to write it after reading that some computers were tested with self-referential programs inspired by the Cretan liar paradox. The writer offered examples such as "This sentence contains five words" as self-referential.

Some very important philosophers such as Wittgenstein, however, and some very unimportant ones, such as I, have argued that self-reference, other than by the writer or speaker in the first person, is illusory. If those computers were being tested by a program that was logically wrong, their results therefore should not have been trusted.

There seems, then, at least to be some limitation to those theorems that humans cannot validate by themselves, since they cannot logically be used as part of the maths for setting up the strategies by which computers check other theorems.

Michael Bulley
Chalon-sur-Saône, France