Simons Institute and SLMath Joint Workshop: AI for Mathematics and Theoretical Computer Science

by Nikhil Srivastava (senior scientist, Simons Institute for the Theory of Computing)

This month, we held a joint workshop with SLMath on AI for Mathematics and Theoretical Computer Science. It was unlike any other Simons Institute workshop I have been to. Over half the participants were mathematicians, and the reception was held up the hill at SLMath to a lovely sunset. But what really set it apart was its afternoons of hands-on tinkering.

In the five-day workshop, there were only 11 talks, held in the mornings. They were about how three kinds of tools — proof assistants, neural networks, and SAT solvers — have led to recent advances in mathematics and computer science. Let me say a bit about these talks to set the scientific context.

Floris van Doorn spoke about an ongoing project to formalize — that is, write in a mechanically verifiable way using the Lean proof assistant — a generalization of Carleson’s theorem, a beautiful and difficult result about pointwise convergence of Fourier series. A big challenge in this process was the tremendous amount of “invisible mathematics” hidden in the human-written proof they started with, in the form of implicit steps and equivalences. It is natural to wonder whether language models will soon be able to translate English proofs into formal proofs in Lean. Several talks during the week pointed to invisible mathematics as a key obstacle to this goal of “autoformalization.” The other obstacle is that while the Lean community has produced a tremendous number of theorems by human standards — 150,000 — this is still very little to train a language model on. 

Some stunning recent advances relied on SAT solvers. Giles Gardam reported on his disproof of an 80-year-old conjecture of Kaplansky on the existence of invertible elements in certain group algebras, via an example found using a SAT solver that he was then able to analyze by hand. Bernardo Subercaseaux mentioned progress on Lam’s conjecture in discrete geometry, where a human-unreadable SAT disproof from 2020 awaits formalization in Lean, displaying the synergy of these tool sets. 

There were talks about producing mathematical objects (rather than proofs) using neural networks. Amaury Hayat explained how neural networks trained on synthetic data were highly successful at finding Lyapunov functions for dynamical systems, beating semidefinite programs and even humans. An (unrecorded) tutorial talk explained how to train a language model to find graphs with many edges and few triangles, which turns out to be remarkably good when combined with a simple local search procedure.

This brings me to the afternoon tutorials. After lunch on the first three days, participants received a worksheet from the organizers on one of the three tools. We opened up our laptops in the Calvin Lab auditorium and did the exercises side by side, with a fleet of TAs among us. We asked each other questions, especially stupid ones. Lots of little conversations happened. 

I had never used Lean or trained a model before. Writing Lean code wasn’t as bad as it initially looked, though I immediately appreciated the “software engineering” difficulties that could arise in a large project. By the end, I could imagine using it in my discrete math class as a model of how to “execute” a proof in your mind. Curious readers should try the Natural Number Game as a gentle introduction. 

Training a model to generate graphs seemed to require a lot more specialized knowledge of PyTorch than I had, so I could do only the easier exercises. But writing the code drove home things that I had heard dozens of times in talks: that the model is approximating a conditional probability distribution, and so on. There was something special about watching many slow iterations of gradient descent. Many participants were surprised by how long it took. I felt like I understood the field better, in my body for the first time. 

Most people I talked to felt like the afternoons were fun, gave them a setting in which to meet new people, and provided an interactive learning experience that talks do not. To all future organizers: please consider having some hands-on activities like these! 

Thanks to SLMath and to the organizers — Jeremy Avigad, Marijn Heule, María Inés de Frutos-Fernández, Adam Zsolt Wagner, Sean Welleck, and Floris van Doorn — for this thoughtful workshop, which required an exceptional effort on their part. We look forward to more joint workshops down the line.