Not the original asker, but I just wanted to appreciate this explanation-simple, concise, but still maintaining a one-to-one correspondence with the actual mathematics. Thank you!
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.
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.
this project focuses only on "1 eq -> 1 eq", so it's even more of a gray area
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