The AI that solved IMO Geometry Problems

Guest video by Aleph0 ​

This is a guest video by Aleph 0, the second in a series of five guest posts this summer while I’m on leave.

This covers AlphaGeometry, a tool for automatically solving most IMO-level geometry problems. But even in the short time since Google DeepMind announced this tool, the abilities of AI in contest and research-level mathematics have come a long way. This year, both DeepMind and OpenAI announced having achieved gold-level performance at the IMO with pure language models.

A project I have in the works for later this year is about the role of AI in modern math. For instance, the loop described in the video above between deductive and intuitive reasoning lends itself very well to math, but it seems the direction the winds are blowing is more towards using the availability of symbolic checkable reasoning on the side of training data generation, more so than during test-time performance.

One aspect of this project will involve interviews with mathematicians about how (if at all) modern reasoning tools are relevant to their work. If you feel you have a story relevant to this, I’d love to hear it, so feel free to fill out this form.