"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.
@tao Although GPT-based content could be very useful, I think the main issue is verifying the authenticity of the proof. I do like your idea of a #GPT including a Lean proof but as you posted not too long ago, the difficulty is making sure that the Lean version is actually proving what is written. I could imagine giving a GPT the #LaTeXmath with the Lean proof and asking it to check if there are any discrepancies, but in my experience neither GPTs nor humans are good at spotting subtle errors.