 Penrose argued that while a formal proof system cannot prove its own consistency, Gödel-unprovable results are provable by human mathematicians.He takes this disparity to mean that human mathematicians are not describable as formal proof systems, and are therefore running a non-computable algorithm.Similar claims about the implications of Gödel's theorem were originally espoused by the philosopher John Lucas of Merton College, Oxford in 1961.