This morning the image reproduced above headed a message I received from info@nationalacademies.org, along with the following text:
Artificial intelligence (AI) has great potential to contribute to mathematical discovery, by guiding conjecture generation, assisting in formalizing mathematics, and more. How are AI technologies being used to advance the mathematical sciences, and how can interdisciplinary collaboration open up new opportunities?
Join the National Academies for a three-part webinar series following on last summer's workshop on AI to Assist Mathematical Reasoning. Each hour-long webinar will delve into a different topic from the workshop: (1) Proof Assistants, (2) the Future of Collaboration, and (3) Machine Learning Approaches to Mathematical Discovery.
If you read the reports on last summer’s workshop published in this newsletter, starting on June 21, 2023 and continuing over five posts through August 3, you might get the impression, on the basis of the questions recorded in my reports, that the audience consisted overwhelmingly of enthusiasts for the mechanization of mathematics; and this may lead you to the conclusion that mathematicians as a whole are overwhelmingly looking forward to the expansion of this new technology. Certainly the panelists, or at least the mathematicians among them, seemed to have been selected exclusively among enthusiasts; only the computer scientists who spoke at the workshop, and then not all of them, occasionally expressed doubts and hesitations. Ahead of the workshop, one mathematician didn’t find this surprising:
when there’s a Sage workshop, we don’t make a point of inviting people who think computer algebra systems are a bad idea… I guess my feeling here is that once the decision has been made to have a workshop about developing this area, it’s gonna have people planning it who think the area is at least probably worth developing.
This colleague saw the stakes of last year’s event as purely technical or informational rather than political. I disagree. I have yet to be convinced that all the attention and resources being devoted to this area by the institutions that support scientific research and by the scientific press is justified by its intrinsic interest for the discipline, rather than the interests of the industry.
I can think of three reasons why so few1 of the audience’s questions raised at last summer’s workshop expressed a critical approach to the prospect of mechanization of mathematics:
The audience was self-selected and consisted primarily or exclusively of “people…who think the area is at least probably worth developing.”
Those mathematicians who did attend and who harbored skeptical thoughts did not feel qualified to question the experts.
The moderators only selected questions that expressed enthusiasm for the technology from among those submitted, either because they felt that only such questions were relevant to the discussion or because they see themselves as part of an embattled minority within mathematics2 struggling against an entrenched and out-of-touch established order.
Conspiracy theorists may be able to come up with additional reasons that I prefer not to entertain in this venue.
So register!
The National Academies published official Proceedings of last summer’s workshop. The 89-page document, which can be downloaded for free at this page, offers a different picture of the event from that reported in this newsletter. I found3 only one reference to “environmental impact” and the “carbon footprint” and one on “corporate interests.” The word “copyright” appears at the bottom every page in the sentence:
Copyright National Academy of Sciences. All rights reserved
but there is no reference to “copyright infringement.” The word “externalities,” on the other hand, does not appear at all.
One reads on p. 8 that the Proceedings were
reviewed in draft form by individuals chosen for their diverse perspectives and technical expertise. The purpose of this independent review is to provide candid and critical comments that will assist the National Academies of Sciences, Engineering, and Medicine in making each published proceedings as sound as possible and to ensure that it meets the institutional standards for quality, objectivity, evidence, and responsiveness to the charge.
If you look at the list of reviewers you will certainly recognize their undeniable technical expertise but you may have to squint to find evidence of “diverse perspectives.” As my colleague wrote, the people reviewing the reports, like those planning the workshop, “think the area is at least probably worth developing.” I’d guess they feel more strongly than that, given that at least three of them, and probably all four, are actively involved in developing precisely this area.
If you are concerned that the discussions sponsored by the NASEM have been one-sided, I encourage you to register for the upcoming webinar series. The speakers, listed below, are among the most qualified to speak on behalf of their perspectives. I hope other perspectives will also be welcomed.
Details about the program follow, with a link for registration at the end of each day’s description.
WEBINAR DATES, TIMES, AND TOPICS:
Proof Assistants: Tuesday, April 23, 2024 from 1-2pm ET
Proof assistants, or interactive theorem provers, are tools that assist in the development of formal mathematical proofs. During this webinar, speakers Adam Chlipala, Massachusetts Institute of Technology, and Timothy Gowers, Collège de France and University of Cambridge, will discuss challenges and opportunities in the design, use, and advancement of proof assistants. Learn more, register, and watch the webinar on the event page.The Future of Collaboration: Wednesday, April 24, 2024 from 1-2pm ET
Machine-assisted mathematical reasoning has drawn interest from various communities grounded in both mathematics and computer science. During this webinar, speakers Lior Horesh, IBM, and Ravi Vakil, Stanford University, will address how collaboration can work between researchers with backgrounds in mathematics, computer science, artificial intelligence, and more. Learn more, register, and watch the webinar on the event page.Machine Learning Approaches to Mathematical Discovery: Thursday, April 25, 2024 from 1-2pm ET
With the rapid growth of machine learning (ML), mathematics research may advance in novel, unexpected ways by adopting ML tools for generating conjectures, developing proofs, and more. During the webinar, speakers Albert Jiang, University of Cambridge, and Christian Szegedy, xAI, will discuss current challenges and opportunities for the advancement of mathematics research using ML tools. Learn more, register, and watch the webinar on the event page.
Maybe zero? I haven’t checked my notes. I did not attend the live (virtual) sessions but I watched the recordings afterwards.
At least one supporter of mechanization has told me that he explicitly identifies as such.
Some appearances of words may be missed because of hyphenation.
Who else---besides me at least---will be attending this week's (second annual) "Cosmic Explorer Symposium," which is being held simultaneously with the NASEM's "Artificial Intelligence to Assist Mathematical Reasoning".
The daily schedules are compatible: first "Cosmic Explorer" 11am-1pm, then "NASEM AI" 1pm-2pm, then "Cosmic Explorer" 3pm-5pm (all timed EDT).
More to the point, the intersectional scientific, engineering, educational, sociological, and political elements that (in coming decades) will challenge the Cosmic Explorer enterprise, span the full range of challenges that AI researchers hope to address.
In a nutshell, Cosmic Explorer is where "the rubber is meeting the road" for AI.
For details of this week's "Cosmic Explorer Symposium," see "https://indico.mit.edu/e/CES2024"