 The Penrose–Lucas argument about the implications of Gödel's incompleteness theorem for computational theories of human intelligence was criticized by mathematicians, computer scientists, and philosophers, and the consensus among experts in these fields is that the argument fails, with different authors attacking different aspects of the argument.LaForte pointed out that in order to know the truth of an unprovable Gödel sentence, one must already know the formal system is consistent.Referencing Benacerraf, he then demonstrated that humans cannot prove that they are consistent, and in all likelihood human brains are inconsistent.