Mathematicians' reactions to AI (and formalization)

[alreadydone]

Background: Mathematicians are listed as the occupation that is most exposed to large language models in research from OpenAI & UPenn: GPTs are GPTs: An Early Look at the Labor Market Impact Potential of Large Language Models.

See also How will AI change mathematics? Rise of chatbots highlights discussion, Feb 2023, Nature (mentions the IPAM workshop and Venkatesh symposium).

Kevin Buzzard on the Sparks of AGI paper:

For example in arguably the hardest math problem they give the system (p40, a modified IMO problem) I have several issues with their presentation. ...

When I was a kid in the early 80s, chess computers had just become viable. ... The only problem was that these chess computers were absolutely lousy at chess. They would never throw away pieces or accidentally let themselves get bank rank checkmated in 1, and they could beat rabbits by simply taking all their pieces and then overwhelming them, but on a reasonably hard setting they were still no match for an average club player, and if you put them on the hardest setting then they typically took hours to make a move. Down my chess club the kids loved them, and the experts showed no interest in them because they had nothing to teach the experts. 15 years later, thanks to IBM (who were at that time a powerhouse in the computing world) who decided to throw a ton of money at the problem, they were beating grandmasters, and since then we've never looked back.

I feel like we're in the "early 80s" phase right now with these large language models, and that is why I am super-uninterested in them right now. I certainly go around giving talks where I extol their virtues, and show a slide where they're solving 50% of the easiest IMO problem ever in Lean and claim that this is a breakthrough (which it is!). But at the end of the day GPT4 getting a half-decent mark in AMC 12, a multiple choice exam meant for schoolkids, is something which can simultaneously be regarded as an amazing achievement and something which indicates that there is still an essentially infinite amount of work still to be done before they are going to be doing research maths, which is why I am still bewildered by the claims of Szegedy¹ et al that this is going to happen by 2029. Right now they can beat rabbits at maths and that's it. Beating rabbits is a major achievement but undergraduates can easily do this too.

Shortly afterwards, Buzzard gave a talk to undergraduate students titled Will Computers Prove Theorems? (slides).²

Abstract: Today we have ChatGPT. In ten years' time will we have a machine where you can type in the statement of the Riemann Hypothesis, press a button, and out pops a correct proof? My guess is no. However in ten years' time will we have machines which can give humans mathematical ideas? Will we have interactive mathematics papers where you can choose the level of detail you want to see in a proof? Will we have machines which understand the state of the art in mathematics? Will mathematicians be being helped by computers in new ways? My guess is that these things are not out of the question. I'll talk about recent developments in AI and in theorem proving software which make me cautiously optimistic.

Now let me collect some reactions to AI from Fields medalists below:

Timothy Gowers is still pursuing his GOFAI approach to automated theorem proving, but he definitely plays a lot with ChatGPT. See also his talk at the Venkatesh symposium.

Terence Tao hosted the Machine Assisted Proofs workshop at IPAM in February (co-organized by Avigad, Buzzard, Jordan Ellenberg, Gowers among others). ChatGPT was a hot topic during the workshop, and Tao has been experimenting with integrating ChatGPT into daily workflow lately³. He also wondered about an automated tool for dependency graph drawing from papers.

Akshay Venkatesh has been thinking about the impact of AI (mechanization) on maths since as early as November 2021, and his Aleph Zero essay was the theme of a symposium held in October 2022 (pre-ChatGPT) organized by Buzzard, Michael Harris⁴ et al. Among the speakers were Avigad, Gowers, Andrew Granville, Geordie Williamson, Emily Riehl, and AI researchers Melanie Mitchell⁵ and Irina Rish. Harris collected participants' impressions in a blog post (and wrote some posts before the symposium as well). Venkatesh has this interesting idea that automated discovery of simplification of proofs could already have a huge impact on the evaluation of mathematical work and people:

Let us suppose that the energies of ℵ(0) are partly directed towards reworking the existing literature: revisiting and supplying proofs of known results rather than examining open questions. As we have emphasized, the number of mathematicians who have thought about a specific question is typically very small, and it is likely that very many parts of the literature would be greatly revised even through careful re-examination by many human mathematicians. It is not unlikely that we will see a scenario that has happened surprisingly rarely in recent history – replacement of long elaborate proofs by short overlooked ones. What effect might a five page combinatorial proof of the Weil conjectures have? Even if such an extreme scenario does not occur, it seems very likely that the web of relationships between standard lemmas and theorems will be altered. This discussion also suggests why the operators of ℵ(0) may be induced to revisit old problems over studying new ones: besides settling concerns about formal correctness, the shifting of foundations has a larger social impact than adding new levels.

Shing-Tung Yau just gave a talk at Fudan University on Friday, and he predicts no substantial change to human social structure within ten years, and top mathematicians won't be affected by AI:

Yau told a reporter from Yicai, "Artificial intelligence is unlikely to have any impact on top mathematicians, but it may have some impact on ordinary mathematicians."
He also predicted that AI would not have a big impact on human social structure within the next ten years, and most of the talk about AI replacing humans is "scaremongering." "Every era of technological change has produced such talk, but in the end, we have always passed through fairly smoothly," Yau told Yicai. "At least in the next ten years, I don't see any substantial changes that AI will make to human society, that is, changes in the entire structure of society."
In an interview with Yicai before the World AI Conference (WAIC) in Shanghai last August, Yau said, "The success of AI is actually a wonderful experience for everyone, but so far no one has been able to deeply explain why AI can be successful."
And this is precisely the path to success for OpenAI, when data accumulates to a certain amount, the ability of AI makes a qualitative leap. Yau once said, "Mathematics should find a way to discover the secrets of why AI is successful."
Six months later, when Yau was asked the same question by Yicai, he said, "A large amount of data will bring about qualitative changes, but qualitative changes are still limited, and I believe that we still need to further study and understand its entire structure."
He emphasized that the limitation of AI is that it can currently only integrate and synthesize a lot of existing data, but it is difficult to make scientific breakthroughs in terms of concepts. This means that AI is still unable to think creatively like humans.

Math Panel with Simon Donaldson, Maxim Kontsevich, Jacob Lurie, Terence Tao, Richard Taylor, and Yuri Milner (interviewer), 2015 Breakthrough Prize Symposium (Nov 10, 2014), Stanford University, https://youtu.be/eNgUQlpc1m0?t=2337 (Fields medalists in bold)

Against formalization:

Efim Zelmanov, On proof and progress in mathematics: the perspective of a research mathematician, in Mathematical Proof Between Generations, July 2022

William Thurston, On proof and progress in mathematics, https://arxiv.org/abs/math/9404236, April 1994 (historical document)

Footnotes

1. Christian Szegedy recently announced he's leaving Google. Is it because he realized we don't need autoformalization to build AGI? What will happen to the N2Formal group? GPT-4 has the multimodal functionality that Szegedy would use to read math papers and autoformalize them, and I definitely would like AGI to help with formalization. Coincidentally, Leonardo de Moura, the father of proof assistant Lean, announced he is moving from Microsoft Research after 17 years to join the Automated Reasoning Group at Amazon Web Services, of which John Harrison, the author of HOL Light, is also a member. ↩

2. Buzzard is a leader in formalization but not in AI; both count as "mechanization" and they could definitely benefit each other, even though the developments so far are mostly independent. It looks like Jemery Avigad is about to publish the article Mathematics and the formal turn on the Bulletin of AMS after publishing Varieties of mathematical understanding (talk) on the same journal last year, and it seems that Johan Commelin and Adam Topaz will publish an account of the now completed Liquid Tensor Experiment on the same issue, which would mark a gain of popularity of formalization among the mathematical community. ↩

3. Picked up by Chinese news outlets: https://www.163.com/dy/article/HVI64N5M0511DSSR.html https://www.jiqizhixin.com/articles/2023-03-06-3 ↩

4. Michael Harris has been writing essays on his blog (Mathematics without Apologies) and Substack (Silicon Reckoner) for years, but often in an obscure style, with philosophical jargons and unfamiliar references to literature that are hard to understand. ↩

5. Not to be confused with Margaret Mitchell, one of the authors of the infamous "Stochastic Parrots" paper. ↩