https://youtu.be/0wL8NlhxXcU AI for the Working Mathematician Speaker: Daniel Litt, University of Toronto Title: Working with LLMs to do high quality math Abstract: Much hay has been made of the capabilities of LLMs to do math autonomously, and indeed frontier models have resolved some long-standing, interesting open questions. But our goal is not to produce papers, but […]
AI for the Working Mathematician Speaker: Akhil Mathew, University of Chicago Title: Finite locally free group schemes Abstract: The notion of a finite locally free group scheme is a natural generalization of the usual notion of a finite group. Lagrange's theorem states that all nth powers vanish in a group of order n. However, this need […]
AI for the Working Mathematician Speaker: Harold Williams, USC Title: An Informal Introduction to Formal Proofs Abstract: In this talk we will give an introduction to Lean, a programming language adapted to expressing and verifying proofs. Lean and its flagship library, mathlib, have been the focus of a dedicated user community for about a decade, […]
AI for the Working Mathematician Speaker: Jordan Ellenberg, University of Wisconsin-Madison Title: Large Hypercubes Abstract: I'll talk about this paper: Bruhat intervals that are large hypercubes <arxiv.org/abs/2601.01235> in which we use a tool from Google, AlphaEvolve, to discover unexpected combinatorial structures inside the symmetric group (to be precise, a large hypercube in the Bruhat order.) I'll […]
AI for the Working Mathematician Speaker: Lauren Williams, Harvard Title: First Proof Batch 3: Mathematicians putting AI to the test Abstract: First Proof is an initiative that aims to obtain a nuanced, objective assessment about the capabilities of large language models to prove specified mathematical statements. I will report on the results of First Proof's third […]