 He argued that mathematicians do not progress by mechanistic search through proofs, but by trial-and-error reasoning, insight and inspiration, and that machines do not share this approach with humans.He pointed out that everyday mathematics can be formalized.He also rejected Penrose's Platonism.