CMU Math Club Colloquium - Ben Przybocki
September 9, 2026 5:30PM—6:45PM
Location:
In Person
-
Porter Hall 100
Speaker:
BEN PRZYBOCKI,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://benprz.com/
Ramsey's theorem is a cornerstone result of mathematics that has spawn an entire area of math called Ramsey theory. In this talk, I introduce Ramsey's theorem and describe a variant that we recently studied by integrating automated reasoning, large language models, and formal verification to accelerate the discovery process. Specifically, Ramsey-good graphs are graphs that contain neither a clique of size s nor an independent set of size t.
We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an s-clique or a t-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In this work, we use LLMs to generate and formalize correctness proofs in Lean.
I hope to convince you that such tool-driven workflows will play an increasingly central role in experiemtnal mathematics.
—
Ben Przybocki is a second-year PhD student in computer science at CMU, advised by Marijn Heule. His primary research interests are in automated reasoning and formal methods. He's especially interested in using SAT and SMT solvers for computer-assisted mathematical discovery.