Open Neighborhood Seminar: Computer Assisted Mathematical Discovery

SEMINARS, OPEN NEIGHBORHOOD

Speaker:

John Mackey - CMU

Chat GPT, AlphaGo, and AlphaGeometry have attracted a lot of attention recently. Computers are getting better and better at problem solving. But what of problem posing? Can computers help us arrive at interesting conjectures and state more nuanced theorems?
In this talk, I'll introduce SAT solvers and talk about their increasing utility in solving combinatorial problems. In particular, we can ask for the minimum number of convex pentagons when n points are placed in the plane in general position. SAT can solve the problem for large enough sets of points that allow us to conjecture the minimum for all n. We'll discuss other open problems and see how SAT may be applied.

===============================

https://people.math.harvard.edu/~gammage/ons/