Gödel’s incompleteness theorems are actually not very relevant to computer formalisation of mathematics. They crushed the naïve hopes of some classical logician

Gödel’s incompleteness theorems are actually not very relevant to computer formalisation of mathematics. They crushed the naïve hopes of some classical logicians in the beginning of the 20th century. But they do not pose any further restrictions on what computer can do, as opposed to what a human can do, with any specific set of axioms.