We recently discussed how advances in technology are contributing to boosting the productivity of mathematicians during the last thirty years. But the chart we featured in that article depicting how the number of math papers being published each month has nearly doubled in the last three years may not do full justice to how fast the pace of new papers coming out has changed.
Another way to communicate that acceleration in output is Matt Parker's approach of focusing on a small subset of the new papers being published in the last few months to show how they represent a big increase in the capability of the AI large language models used to generate their findings. In the following video, in what is becoming an annual tradition, he interrupts his vacation to cover breaking news in the world of mathematics.
Parker makes an explicit point of noting the use of the Lean proof assistant to verify their findings, which gives greater confidence the findings in these papers will stand up to serious scrutiny.
Not all the preprint papers that have recently populated the mathematics category of the arXiv database meet that standard, as Reddit math community poster Salt_Attorney recently observed.
By contrast, Lean verification was used in the ten advances spanning several disciplines in mathematics OpenAI claims its Astra AI system has made. As such, they have a much better chance they'll be found valid when the findings are reviewed.
But the question now being raised is whether verification of findings by a proof assistant is enough to accept AI-generated results as presented. For further reading on that topic, we'll recommend Gary Marcus' discussion of OpenAI's claimed accomplishment to appreciate it may not be either as grand or the Astra AI system as capable as presented in OpenAI's announcement.