Computer search in pure mathematics

Abstract:
Computation-intensive approaches to problems in pure mathematics have a long history, c.f. the 4-color theorem and Hales' proof of the Kepler conjecture. The latest advancements in computer search methods and available computational resources provide an additional impetus to these approaches. The talk will showcase some of our work in this vein, including:

- Resolving Erdős' conjecture that the density of a measurable planar set avoiding unit distances cannot reach 1/4 [1].
- Establishing upper and lower bounds on the number of straight lines needed to slice all cells of an n x n square grid [2].

More broadly, the talk will include a brief introduction to the work done by the Rényi Institute AI research group, placing it in the context of recent developments in AI.