We discuss Kunen’s algorithmic implementation of a proof for the Paris–Harrington theorem, and the author’s and da Costa’s proposed “exotic” formulation for the P =  NP hypothesis. Out of those two examples we ponder the relation between mathematics within an axiomatic framework, and intuitive or informal mathematics.