AI to Assist Mathematical Reasoning: A Workshop

Thanks PROF

Thanks for organizing this workshop. A few comments:
* Funding sources identified: Microsoft, Google, DARPA, Simons Foundation. Why does this matter? A key worker in the field complained recently that funding had dried up for interactive theorem proving, that AMS prioritized automated theorem proving over interactive theorem proving, and that mathematicians who originate new proofs in Math departments didn’t respect people who “just” worked on mechanically verifying those proofs. The people who do Lean and Coq need support or the projects could die out.
* Key use case (and maybe opportunity for funding): AMS and similar should encourage and incentivize mathematicians to use Lean or Coq to formally check their new proofs. Why? (a) Wiles’ proof of FLT took several years for mathematicians to have faith in it. A formally verified proof would take 0 years and 0 faith to accept. (b) It was noted that Wiles’ proof has a lot of “weasel words” like “analogous to” for constructions. With an interactive theorem proof, Wiles’ would have been forced to make these mappings explicit. (c) Some claim that no one mathematician, including Wile, has the whole proof of FLT in their heads. Is this true? Making mathematicians “program” their proofs in Coq or Lean would help suss this out. Mathematicians already use LaTeX all the time. There is no reason they should add Coq or Lean to their toolkit for daily use.
* So Terry, please learn Lean and start doing some proofs in Lean. It will be a great experience for you, and that will help you guide the AI/Math field. Maybe you can do FLT? It’s been waiting for 28 years for fully automated verification. You could do it in 2 weeks. You will be modelling this for other mathematicians. There is really a huge social gap between “mathematician’s mathematicians” doing pure math for math’s sake, and people who do automated theorem proving.
* AI? Meh. GPT doesn’t have the necessary structure to learn this material. People didn’t really talk about what it would take to extend it. Formally verifying proofs is computationally hard, depending on the number of variables in a goal state of the proof, even when you do it directly and as efficiently as you know how.