{"id":247044,"date":"2025-09-22T19:36:18","date_gmt":"2025-09-22T19:36:18","guid":{"rendered":"https:\/\/www.europesays.com\/us\/247044\/"},"modified":"2025-09-22T19:36:18","modified_gmt":"2025-09-22T19:36:18","slug":"mit-affiliates-win-ai-for-math-grants-to-accelerate-mathematical-discovery-mit-news","status":"publish","type":"post","link":"https:\/\/www.europesays.com\/us\/247044\/","title":{"rendered":"MIT affiliates win AI for Math grants to accelerate mathematical discovery | MIT News"},"content":{"rendered":"

MIT Department of Mathematics researchers David Roe<\/a> \u201906 and Andrew Sutherland<\/a> \u201990, PhD \u201907 are among the inaugural recipients of the Renaissance Philanthropy and XTX Markets\u2019 AI for Math grants<\/a>.\u00a0<\/p>\n

Four additional MIT alumni \u2014 Anshula Gandhi \u201919, Viktor Kun\u010dak SM \u201901, PhD \u201907; Gireeja Ranade \u201907; and Damiano Testa PhD \u201905 \u2014 were also honored for separate projects.<\/p>\n

The first 29 winning projects will support mathematicians and researchers at universities and organizations working to develop artificial intelligence systems that help advance mathematical discovery and research across several key tasks.<\/p>\n

Roe and Sutherland, along with\u00a0Chris Birkbeck<\/a>\u00a0of the University of East Anglia,\u00a0will use their grant\u00a0to boost automated theorem proving by building connections between the\u00a0<\/a>L-Functions and Modular Forms Database<\/a>\u00a0(LMFDB) and the\u00a0<\/a>Lean4 mathematics library<\/a>\u00a0(mathlib).<\/p>\n

\u201cAutomated theorem provers are quite technically involved, but their development is under-resourced,\u201d says\u00a0Sutherland. With AI technologies such as large language models (LLMs), the barrier to entry for these formal tools is dropping rapidly, making formal verification frameworks accessible to working mathematicians.\u00a0<\/p>\n

Mathlib is a large, community-driven mathematical library for the\u00a0Lean<\/a>\u00a0theorem prover, a formal system that verifies the correctness of every step in a proof.\u00a0Mathlib currently contains on the order of 105 mathematical results (such as lemmas, propositions, and theorems). The LMFDB,\u00a0a massive, collaborative online resource that serves as a kind of \u201cencyclopedia\u201d of modern number theory,\u00a0contains more than 109 concrete statements.\u00a0Sutherland\u00a0and Roe are managing editors of the LMFDB.<\/p>\n

Roe and Sutherland\u2019s grant will be used for a\u00a0project that aims to augment both systems, making the LMFDB\u2019s results available within mathlib as assertions that have not yet been formally proved, and providing precise formal definitions of the numerical data stored within the LMFDB. This bridge will benefit both human mathematicians and AI agents, and provide a framework for connecting other mathematical databases to formal theorem-proving systems.<\/p>\n

The main obstacles to automating mathematical discovery and proof are the limited amount of formalized math knowledge, the high cost of formalizing complex results, and the gap between what is computationally accessible and what is feasible to formalize.<\/p>\n

To address these obstacles, the researchers will use the funding to build tools for accessing the LMFDB from mathlib, making a large database of unformalized mathematical knowledge accessible to a formal proof system. This approach enables proof assistants to identify specific targets for formalization without the need to formalize the entire LMFDB corpus in advance.<\/p>\n

\u201cMaking a large database of unformalized number-theoretic facts available within mathlib will provide a powerful technique for mathematical discovery, because the set of facts an agent might wish to consider while searching for a theorem or proof is exponentially larger than the set of facts that eventually need to be formalized in actually proving the theorem,\u201d says Roe.<\/p>\n

The researchers note that proving new theorems at the frontier of mathematical knowledge often\u00a0involves steps that rely on a nontrivial computation. For example, Andrew Wiles\u2019 proof of Fermat\u2019s Last Theorem uses what is known as the \u201c3-5 trick\u201d at a crucial point in the proof.<\/p>\n

\u201cThis trick depends on the fact that the modular curve X_0(15) has only finitely many rational points, and none of those rational points correspond to a semi-stable elliptic curve,\u201d according to\u00a0Sutherland. \u201cThis fact was known well before Wiles\u2019 work, and is easy to verify using computational tools available in modern computer algebra systems, but it is not something one can realistically prove using pencil and paper, nor is it necessarily easy to formalize.\u201d<\/p>\n

While formal theorem provers are being connected to computer algebra systems for more efficient verification, tapping into computational outputs in existing mathematical databases offers several other benefits.<\/p>\n

Using stored results leverages the thousands of CPU-years of computation time already spent in creating the LMFDB, saving money that would be needed to redo these computations. Having precomputed information available also makes it feasible to search for examples or counterexamples without knowing ahead of time how broad the search can be. In addition, mathematical databases are curated repositories, not simply a random collection of facts.\u00a0<\/p>\n

\u201cThe fact that number theorists emphasized the role of the conductor in databases of elliptic curves has already proved to be crucial to one notable mathematical discovery made using machine learning tools:\u00a0murmurations<\/a>,\u201d says\u00a0Sutherland.<\/p>\n

\u201cOur next steps are to build a team, engage with both the LMFDB and mathlib communities, start to formalize the definitions that underpin the elliptic curve, number field, and modular form sections of the LMFDB, and make it possible to run LMFDB searches from within mathlib,\u201d says Roe. \u201cIf you are an MIT student interested in getting involved, feel free to reach out!\u201d\u00a0<\/p>\n","protected":false},"excerpt":{"rendered":"MIT Department of Mathematics researchers David Roe \u201906 and Andrew Sutherland \u201990, PhD \u201907 are among the inaugural…\n","protected":false},"author":3,"featured_media":247045,"comment_status":"","ping_status":"","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[21],"tags":[691,131285,131291,738,131286,131292,131287,131289,131288,131290,131282,131283,158,67,132,68,131284],"class_list":{"0":"post-247044","1":"post","2":"type-post","3":"status-publish","4":"format-standard","5":"has-post-thumbnail","7":"category-artificial-intelligence","8":"tag-ai","9":"tag-ai-for-math","10":"tag-andrew-sutherland","11":"tag-artificial-intelligence","12":"tag-automated-theorem-proving","13":"tag-david-roe","14":"tag-l-functions-and-modular-forms-database","15":"tag-lean4-mathematics-library","16":"tag-lmfdb","17":"tag-mathlib","18":"tag-mit-mathematics","19":"tag-renaissance-philanthropy","20":"tag-technology","21":"tag-united-states","22":"tag-unitedstates","23":"tag-us","24":"tag-xtx-markets"},"share_on_mastodon":{"url":"https:\/\/pubeurope.com\/@us\/115249635875774168","error":""},"_links":{"self":[{"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/posts\/247044","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/comments?post=247044"}],"version-history":[{"count":0,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/posts\/247044\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/media\/247045"}],"wp:attachment":[{"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/media?parent=247044"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/categories?post=247044"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.europesays.com\/us\/wp-json\/wp\/v2\/tags?post=247044"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}