Introducing Aristotle: AI, Formal Methods, and the Future of Mathematical Collaboration

Abstract: Over the past year, Aristotle, a new system combining formal methods and language modeling, has achieved gold-medal level performance at the IMO, solved open conjectures, and opened up a strange new way of working with math. This talk will explain the technology behind Aristotle and present a vision for how mathematicians and AI might organize very large-scale collaborations. We'll also give a brief tutorial on using Aristotle to interactively prove theorems, formalize papers, and explore theories.