The link: Machine assisted proof, a text version of a recent talk by Terence Tao.
The who: Tao is acknowledged as one of the best mathematicians in the world, active not just at the cutting edge of research but also working on, exploring, and explaining the process of research itself. Besides theoretical research, he has spearheaded some recent projects on automated proof checking of recent “real world” theorems.
The what: The talk looks at what you can call “the use of AI in mathematical research,” in particular machine learning, formal proof assistants, and large language models, both as individual technologies and in their potential working together. I think a fair summary of his position is that they are already useful in some ways now, and might plausibly become much more so in the future: not as “autonomous AI super-mathematicians” but as tools that can enhance the productivity of mathematical researchers.
The takeaway: This might not seem an Earth-shattering take, but mathematical research is one of the foundations of scientific and technological advancements, so if one of the foremost mathematicians in the world says he thinks these tools are useful and might become even more so, that’s rather good news, and highlights the impact of the use of AI not to replace experts with lower-paid people (or not at all), but to make the best even better; at that margin, every small improvement becomes huge over time.