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.
Comments
Holy smokes thank you!!! Yeah that makes much more sense now. Thank you for taking the time to write all that up!
Would Godel’s incompleteness theorem throw a monkey wrench into some of this effort? Probably not Tao would have already thought of that I guess.
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:
Even though the general problem is undecidable, individual instances are still potentially solvable.
I remark that it's the "several equations -> several equations" that's undecidable
this project focuses only on "1 eq -> 1 eq", so it's even more of a gray area
Awesome thanks for clarifying
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