> Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems Human ma

> Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems Human mathematicians are equally limited by Gödel.