From September 14th to 16th, the ICMAT hosted the 'AI in Mathematics days' workshop, an event that gathered more than 100 researchers, both in person and remotely. The focus was on the use of artificial intelligence (AI) tools in mathematical research and the formalization of proofs.
The recent news about OpenAI's potential breakthrough in solving the Navier-Stokes equations, one of the Millennium Problems, has marked a significant milestone. Researchers like Diego Córdoba (CSIC at ICMAT) and Luis Martínez-Zoroa (CUNEF University) have indicated that this event signifies the beginning of a completely new era in mathematical research.
The workshop program featured three mini-courses delivered by international experts: María Inés de Frutos Fernández (Universität Bonn), Damien Galant (Brown University), and Mitchell Taylor (Oxford University). Taylor provided a general overview of AI tools applied to mathematical work. Videos of these courses will soon be available on the ICMAT YouTube channel.
Alberto Enciso and Ángel Castro, both from CSIC at ICMAT and organizers of the event, commented that the use of AI is expanding the scope of mathematical work and other fields, altering both the methods and the objectives of research.
A central theme of the meeting was the formalization of mathematical proofs using programs like Lean. This tool allows for the automatic verification of proof correctness, offering a "superhuman guarantee," according to De Frutos Fernández, a specialist in the field. AI, while capable of generating new proofs, requires this formalization to ensure its validity.
Formalization tools, such as Lean, also facilitate a deeper understanding of the underlying theory and promote the development of reusable libraries of formalized mathematics. Other proof assistants mentioned include Rocq, Isabelle, Mizar, and Metamath, each with specific applications depending on the research area.
