From 14 to 16 September, ICMAT organised the workshop AI in Mathematics days at ICMAT, which brought together more than 100 researchers both in person and online. Three courses were held on the use of artificial intelligence tools in mathematical research, as well as on mathematical formalisation, led by international researchers.
ICMAT hosted the workshop AI in Mathematics days at ICMAT. Image: Laura M. Iraola/ICMAT
A few days ago, mathematical research was confronted with news that made headlines around the world: technology company OpenAI announced a possible solution, using artificial intelligence (AI) tools, to one of the seven Millennium Prize Problems, selected as such by the Clay Mathematics Foundation in 2000 and carrying a one-million-euro prize: the Navier–Stokes equations. “What has happened shows that we are entering a completely new stage of mathematical research,” reflected Diego Córdoba, CSIC Research Professor at ICMAT, and Luis Martínez-Zoroa, professor and researcher at CUNEF Universidad and a former doctoral student of Córdoba, who developed a mathematical strategy that has been recognised as a precursor to OpenAI’s proposal.
From 14 to 16 September, more than 100 mathematicians interested in discovering the possibilities offered by AI at different stages of research work in this new stage attended the workshop AI in Mathematics days at ICMAT. The programme consisted of three mini-courses, delivered by María Inés de Frutos Fernández (Universität Bonn), Damien Galant (Brown University) and Mitchell Taylor (Oxford University). The latter gave a general overview of the different artificial intelligence tools used in mathematical work. Videos of the mini-courses will be available on the ICMAT YouTube channel shortly.
The meeting brought together more than 100 mathematicians interested in discovering the possibilities offered by AI at different stages of research work. Image: Laura M. Iraola/ICMAT
“The use of AI changes the scope of our work, in mathematics and in almost every other field, although the change should not be limited to the way we proceed, but should also affect the very objectives that we pursue and value,” comments Alberto Enciso, CSIC Research Professor at ICMAT and one of the conference organisers, together with Ángel Castro, CSIC Research Scientist at ICMAT.
Mathematical formalisation
One of the main topics addressed at the meeting was the formalisation of mathematical proofs using the Lean programme, whose main advantage is that it can automatically check whether a proof is correct. The programme works by checking, based on a list of axioms and rules, whether a proof follows them. “What you are doing is giving yourself a superhuman guarantee that a mathematical proof is correct,” explains De Frutos, a specialist in mathematical formalisation.
Mª Inés de Frutos (University of Bonn) delivered one of the three courses at the workshop. Image: Laura M. Iraola/ICMAT
This is particularly interesting when combined with AI tools, such as language models, which appear to be capable of writing new proofs of open results. “A proof of a result obtained by AI is not necessarily correct. But we can find out whether it is by formalising it in a language such as Lean,” explains De Frutos.
But mathematical formalisation tools go further. “Even when using this programme, we can gain a better understanding of the theory underlying a piece of research, because it requires a great deal of detail,” she continues. “It is also highly beneficial for the community to develop large libraries of formalised mathematics for subsequent projects. Formalisations of definitions and theorems can be reused and built upon,” says De Frutos.
Although it is the most widely used in the mathematical community, Lean is one of several proof assistants available. Others, such as Rocq, Isabelle, Mizar and Metamath, may be more suitable depending on the area of research to be formalised. “For example, if you want to carry out software verification rather than theorem verification, Rocq is very popular. It depends on the foundations and the community,” explains the mathematician, whose course focused on this programme, as did Taylor’s, which placed greater emphasis on its application to analysis and partial differential equations.
—
This text is an automatic translation from the original Spanish version.