Informal versus formal mathematics

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. The author is Visiting Researcher at IEA/USP, Professor of Communications, Emeritus, at the Federal University in Rio de Janeiro, and a full member of the Brazilian Academy of Philosophy.