&gt;&gt; Russell realized this, and recognized that Gödel&#x27;s results invalidated his project.<p>&gt; One particular project.<p>A mathematical proof applies to all cases, not just one. Gödel&#x27;s result addressed Russell&#x27;s project, but it applies universally, as do all valid mathematical results. Many mathematicians regard Gödel&#x27;s result as the most important mathematical finding of the 20th century.<p>&gt; That doesn&#x27;t mean we&#x27;ve stopped doing math.<p>Not the topic.<p>&gt; A human can look at Coq and say &quot;Yes, this is correct&quot; or &quot;No, this is wrong&quot; just fine, without running afoul of the halting problem, Gödel&#x27;s incompleteness theorem, or anything else.<p>This is false. If the Halting problem is insoluble, it is also insoluble to a human, and perhaps more so, given our tendency to ignore strictly logical reasoning. It places firm limits on what we can claim to have proven. Surely you aren&#x27;t asserting that human thought transcends the limits of logic and mathematics?<p>&gt; Of course they&#x27;ve proven things just fine if they&#x27;re able to convince other human mathematicians that they&#x27;ve proven things.<p>Yes, with the caution that the system they&#x27;re using (and any such system) has well-established limitations as to what can be proven. You may not be aware that some problems have been located that validate Gödel&#x27;s result by being ... how shall I put this ... <i>provably unprovable</i>. The Turing Halting problem is only one of them, there are others.