Also, humans often believe things that aren't provable in any formal system S because they're not true. Even good mathematicians believe (hopefully temporarily)

Also, humans often believe things that aren't provable in any formal system S because they're not true. Even good mathematicians believe (hopefully temporarily) false propositions. So the argument "some true things are not provable by formal logic in S, therefore if a human can believe something not provable in S, they must not be a formal system" is valid, but does not imply "no machine can be constructed that believes something not provable in S" since a little sprinkling of randomization can make anything possible. A machine that can prove any true proposition with p>2/3 and only believes false propositions with p<1/3 would be pretty useful.