Some practical tips on digesting AI proofs: informal and formal aspects

Abstract: In this new era of proof abundance, "digestion" has become an important part of mathematics. As of October 2026, LLM-generated proofs are still hard to read, and making them accessible requires considerable effort. On August 1, OpenAI announced a result on the optimal exponent for both the Cohn–Elkies linear programming bound and the Bourgain–Clozel–Kahane sign uncertainty principle. In this talk, I will share my experience digesting this result. We will also go through its formalization and how it can be improved.

machine learningcombinatoricsnumber theory

Audience: researchers in the topic

AI, Combinatorics and Number Theory Seminar

Series comments: This seminar is devoted to the responsible and constructive use of AI in number theory and combinatorics. It is a space to think carefully about what these tools can and cannot do, and where the limits actually lie. Enthusiasm and skepticism are both welcome here, and we ask only that they be voiced with generosity. Questions from students and from people new to these areas are especially encouraged.

The seminar meets Online via Zoom from 2:00 PM – 3:00 PM Eastern Time.

Please email the organizers to join the mailing list and receive the Zoom links.