Return to Colloquia & Seminar listing
A renewed attack on the four color theorem
Geometry/Topology| Speaker: | Dan Romik, UC Davis |
| Location: | 2112 MSB |
| Start time: | Tue, May 26 2026, 2:10PM |
Description
The Four Color Theorem ("4CT") states that any loopless planar graph can be colored with four colors. Despite the fact that the theorem was proved in 1976 by Appel and Haken, and reproved several times since (using ideas that are substantially similar to those used by Appel and Haken), the state of our knowledge on the theorem is still unsatisfactory: all known proofs are heavily computer assisted and rely on large and fragile certifying datasets and on complicated software that verifies the theorem from the dataset. In this talk I will give an inconclusive update on my recent attempts to find more robust proofs of 4CT using modern AI, machine learning, and software development tools. I will also discuss some broader questions this project raises, such as: is what I am doing actually a form of math research? Or is it software engineering, or something else? Is this type of work what we should expect much or even all math research to look like in the near future? And more.