Matematycy z MIT otrzymali grant AI for Math na stworzenie pomostu między bazami danych a weryfikatorami twierdzeń

MIT mathematicians David Roe and Andrew Sutherland have been named recipients of the AI for Math grants, an inaugural funding scheme launched by Renaissance Philanthropy and XTX Markets. As members of MIT’s Department of Mathematics, they’re going to take this opportunity to blend artificial intelligence with groundbreaking mathematical research.

This new initiative aims to propel mathematical discovery by funding 29 pioneering projects, each tasking AI to reshape the field of mathematics. It’s all about giving mathematicians the tools to develop AI systems that boost discovery speed and enhance formal reasoning in a wide array of mathematical areas.

As part of this impressive rollout, Roe and Sutherland, working alongside Chris Birkbeck from the University of East Anglia, are planning to use their grant to connect two major mathematical resources: the L-Functions and Modular Forms Database (LMFDB) and the Lean4 mathematics library (mathlib).

Bridging Mathematical Realms with AI

On one hand, the mathlib, a comprehensive library driven by a massive international community, uses the Lean theorem prover to verify the validity of each logical step in a proof. With about 100,000 mathematical results, it’s basically a goldmine of mathematical findings.

On the other hand, there’s the LMFDB, a mammoth digital encyclopedia of modern number theory. Housing over a billion mathematical statements and data points, it’s a go-to-resource for professional and aspiring mathematicians alike. Making sense of this colossal data mountain is a daunting task, but with Roe and Sutherland serving as the LMFDB’s managing editors, they’re just the right people for the job.

Demystifying Mathematics with AI

The traditional learning path to understanding automated theorem provers is steep, admits Sutherland. However, due to the increasing availability and effectiveness of large language models (LLMs) and other AI tools, the learning process has become less intimidating, inviting a wider audience of mathematicians to use these systems.

The primary goal here is to avail the LMFDB’s vast number-theoretic facts to mathlib. This integration would open up unrestricted exploration of the mathematical universe to both AI agents and human mathematicians. To achieve this, the team is not planning on formalizing the whole LMFDB – which would be extremely labor-intensive – rather, they aim to develop tools that selectively tap into its contents. The tactic, expected to cut costs, implies that not all of the information required for establishing new theorems has to be formally proved.

Modern mathematical theorems, such as Andrew Wiles’ proof of Fermat’s Last Theorem, lean heavy on computational steps which are not so simple to formalize by hand. This is exactly why mathematical databases like the LMFDB are invaluable and serve as crucial resources to mathematicians.

The importance of curation in mathematical databases can’t be overstated. For instance, the LMFDB’s focus on the conductor in elliptic curves was pivotal in the recent identification of elliptic curve murmurations, a phenomenon discovered using machine learning techniques.

Building the Future of Mathematics

Roe and his team intend to start the whole endeavor by formalizing the definitions that underpin the LMFDB’s elliptic curve, number field, and modular form sections and allow execution of LMFDB searches within mathlib. Their plan opens up opportunities for students at MIT to be part of this grand mathematical adventure.

In addition to Roe and Sutherland, four other mathematics trailblazers from MIT—Anshula Gandhi, Viktor Kunčak, Gireeja Ranade, and Damiano Testa—have been awarded the AI for Math grants in recognition of their innovative work in the field.

For more on the AI for Math grants, check out the full article tutaj.