There is no a priori reason why the aimed for results should be unprovable ala Gödel.

However, it turns out it has been proven that it is. Tao says so in the post:

> I will remark that the general question of determining whether one set of equational axioms determines another is undecidable.

Even though the general problem is undecidable, individual instances are still potentially solvable.

A really good question! I've been out of the field for a long time, but it's important to stress the difference between "interactive proof assistants" and "automated theorem provers." The latter consist in various software tools that, given a well-formed logical formula, attempt to automatically derive a proof thereof in a given logic. There are of course well-understood limits to such tools given the foundational results of Gödel, Turing etc in the early 20th century.

On the other hand, interactive proof assistants such as Lean, mentioned in the title article, or Isabelle are really something more like functional programming languages in which a human mathematician can specify and prove a given theorem, relying on the work of other mathematicians as equivalent to a third-party library. Again like with programming languages, the different tools will offer various trade-offs between expressibility and the kinds of guarantees that can be made at compile time about the validity of a proof. It has traditionally been viewed as far too time consuming to actually specify even intermediate mathematics in such tools, but LLMs really change the situation, as Terrance Tao in particular has demonstrated.

For anyone interested in the topic, I highly recommend the work of the CMU logician Jeremy Avigad. See, for example: * Formally Verified Mathematics- https://www.andrew.cmu.edu/user/avigad/Papers/cacm.pdf * Automated Reasoning in Mathematics- https://link.springer.com/chapter/10.1007/978-3-031-63498-7_... * The Mechanization of Mathematics- https://www.ams.org/journals/notices/201806/rnoti-p681.pdf