AI and Mathematics Seminar

Abstract. We'll do a "show and tell" of what it's like to try to formalize some basic mathematics in Lean, with help from AI.

• Recording, Passcode: g&CcN6n=

Abstract. In this talk, I’ll provide an overview of some advancements in AI and machine learning in proof assistant languages, such as Lean, Rocq, and Isabelle/HOL. I’ll discuss both neural and symbolic techniques for various proof assistant tasks, including automated proof synthesis, autoformalization, premise selection, and lemma conjecturing. With respect to neural techniques, I’ll cover the basics of applying language models, reinforcement learning, and graph neural networks to the theorem proving domain.

• Recording , Passcode: v8c%A!&8

Abstract. This talk introduces Goedel-Prover-V2, an open-source model that sets a new state of the art in automated theorem proving.

Abstract. We seek algorithms for program learning that are both sample-efficient and computationally feasible. Classical results show that targets admitting short program descriptions (e.g., with short "python code") can be learned with a "small" number of examples (scaling with the size of the code) via length-first program enumeration, but the search is exponential in description length. Consequently, Gradient-based training avoids this cost yet can require exponentially many samples on certain short-program families.

To address this gap, we introduce LLM-ERM, a propose-and-verify framework that replaces exhaustive enumeration with an LLM-guided search over candidate programs while retaining ERM-style selection on held-out data. Specifically, we draw k candidates with a pretrained reasoning-augmented LLM, compile and check each on the data, and return the best verified hypothesis, with no feedback, adaptivity, or gradients. Theoretically, we show that coordinate-wise online mini-batch SGD requires many samples to learn certain short programs. Empirically, LLM-ERM solves tasks such as parity variants, pattern matching, and primality testing with as few as 200 samples, while SGD-trained transformers overfit even with 100,000 samples. These results indicate that language-guided program synthesis recovers much of the statistical efficiency of finite-class ERM while remaining computationally tractable, offering a practical route to learning succinct hypotheses beyond the reach of gradient-based training.

Abstract. We introduce an LLM + computer software framework for proving sophisticated inequalities in research mathematics. We first ask a frontier LLM to break up a problem into its simplest parts, and then ask a computer algebra system to complete the proof for each part. In doing so, we solve a concrete question posed by Terence Tao. This is joint work with Vijay Ganesh (Georgia Tech).