#ScientificAmerican recently reprinted an interview I had a few months ago on the future of proof assistants and #AI in #math: https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/ . In it, I made the following assertion:
"I think in the future, instead of typing up our proofs, we would explain them to some #GPT. And the GPT will try to formalize it in #Lean as you go along. If everything checks out, the GPT will [essentially] say, “Here’s your paper in #LaTeXmath; here’s your Lean proof. If you like, I can press this button and submit it to a journal for you.” It could be a wonderful assistant in the future."
This statement seems to have received a mixed reception, in particular it has been interpreted as an assertion that mathematicians would be become lazier and sloppier with writing proofs. I think the best way to illustrate what I mean by this assertion is by a worked example, which is already within the capability of current technology. At https://terrytao.wordpress.com/2016/10/18/a-problem-involving-power-series/ I have a moderately tricky problem in complex analysis. In https://chatgpt.com/share/63c5774a-d58a-47c2-9149-362b05e268b4 , I explained this problem and its solution to #ChatGPT in an interactive fashion, and after the proof was explained, GPT was able to provide a LaTeX file of the solution, which one can find at https://terrytao.wordpress.com/wp-content/uploads/2024/06/laplace.pdf . GPT performed quite well in my opinion, fleshing out my sketched argument into quite a coherent and reasonably rigorous full proof. This is not 100% of what I envisioned in the article - in particular the rigorous Lean translation in order to guarantee correctness is missing, which I think is an essential requirement before this workflow can be used for research quality publications - but hopefully will illustrate what I had in mind with the quote.
