1. The letter (dated August 31, 1965) from Morris Kline at NYU is available in Lakatos File 13/485.

2. It is worth noting that in some cases in mathematics the distinction between context of discovery and context of justification may be very blurry. Thus in set theory, the ‘discovery’ of a new axiom about real numbers, such as the axiom of definable determinacy, is typically the end process of a long period of working with the candidate axiom and examining its consequences. Moreover its status as an axiom may rest at least in part on arguments that it is in some sense ‘inevitable.’

3. A potential example of an unformalizable element of a proof may arise in connection with the Church-Turing thesis, since the notion of ‘algorithm’ is widely held to have no satisfactory formal definition.

4. Fallis adds that this kind of gap is typically marked by “the ever-recurring phrase ‘It is easy to see that …’ .”

5. See Tennant (2005) for a useful recent discussion of this issue.

6. A good source for more details on Plateau’s experiments is Courant & Robbins (1941, 386–397).

7. In fact, Goldbach made a slightly more complicated conjecture which has this as one of its consequences.

8. Frege: it is difficult to find “even a single common property which has not actually to be first proved common” (Foundations of Arithmetic, p. 15).

9. cf. Wang’s Paradox—discussed, for example, by Dummett (1974).

10. Here ‘↑’ denotes the exponentiation function, and these are evaluated from right to left. For more on this example, see te Riele (1987).

11. Of course, given the enormous power of modern computers in comparison to pencil-and-paper calculations, it would not be surprising to find experimental mathematics dominated by computers regardless of whether this is (theoretically speaking) an essential feature of the subfield.

12. Nor is unsurveyability solely a property of computer-based proofs. For example, the classification of all finite simple groups was the result of a collaboration of many mathematicians over several decades, without any essential use of electronic computers, that resulted in a proof that runs to thousands of pages spread over different journal issues and is effectively unsurveyable by any single human mathematician.