{"686371":{"#nid":"686371","#data":{"type":"news","title":"Anton Leykin Awarded AI for Math Fund Grant","body":[{"value":"\u003Cp dir=\u0022ltr\u0022\u003ESchool of Mathematics Professor\u003Ca href=\u0022https:\/\/research.gatech.edu\/people\/anton-leykin\u0022\u003E\u0026nbsp;\u003Cstrong\u003EAnton Leykin\u003C\/strong\u003E\u003C\/a\u003E is part of a research team selected to receive support through the \u003Ca href=\u0022https:\/\/www.renaissancephilanthropy.org\/initiatives\/ai-for-math-fund\u0022\u003EAI for Math Fund\u003C\/a\u003E, a new grant program created to accelerate the development of artificial intelligence (AI) and machine learning tools for mathematics.\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003E\u201cThis grant gives me a foothold in a new world where AI can be used in a very concrete way,\u201d says Leykin. \u201cIt\u2019s an opportunity to move beyond the hype and develop tools that truly benefit mathematical research.\u201d\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003EWith a total of $18 million in inaugural grants to 29 project teams, the AI for Math Fund backs initiatives that create open-source tools, expand high-quality datasets for AI training, and make advanced systems more accessible to mathematicians.\u0026nbsp;The fund received 280 grant applications from researchers and mathematicians worldwide.\u0026nbsp;\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003E\u003Cstrong\u003EBuilding bridges\u003C\/strong\u003E\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003ELeykin\u2019s global team includes researchers from the University of South Carolina, University of Warwick, and Cornell University. Their project,\u0026nbsp;\u003Cstrong\u003E\u201c\u003C\/strong\u003E\u003Ca href=\u0022https:\/\/www.renaissancephilanthropy.org\/bridging-proof-and-computation-a-verified-leanmacaulay2-interface\u0022\u003E\u003Cstrong\u003EBridging Proof and Computation: For a Verified Lean-Macaulay2 Interface\u003C\/strong\u003E\u003C\/a\u003E\u003Cstrong\u003E,\u201d\u003C\/strong\u003E aims to connect two powerful systems: Lean, a platform for assisting and formalizing mathematical proofs, and Macaulay2, a computational algebra system widely used in research.\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003EBy developing a native interface \u2014\u0026nbsp;a built-in connection that allows the two systems to work together without external tools \u2014\u0026nbsp;and a Lean-based domain-specific language, the project will enable communication between these systems. This will allow Lean users to formulate tactics that involve sophisticated computation done by algorithms implemented in Macaulay2; in return, Macaulay2 users can formalize computer-assisted proofs via Lean with a little help from AI.\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003E\u201cThis integration has the potential to transform how mathematicians work,\u201d says Leykin. \u201cIt will not only connect Lean and Macaulay2 but also lay the groundwork for a general interface that could benefit other computer algebra systems in the future.\u201d\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003EHis goal is to create a robust proof-assistance system where AI can help generate strategies and validate proofs, driving progress in areas that require both computational power and rigorous verification.\u003C\/p\u003E\u003Cp dir=\u0022ltr\u0022\u003E\u003Cstrong\u003EAbout the AI for Math Fund\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003EA joint initiative developed in partnership between\u003Ca href=\u0022https:\/\/renaissancephilanthropy.org\/\u0022\u003E\u0026nbsp;Renaissance Philanthropy\u003C\/a\u003E and founding donor\u003Ca href=\u0022https:\/\/www.xtxmarkets.com\/\u0022\u003E\u0026nbsp;XTX Markets\u003C\/a\u003E, the AI for Math Fund is one of the largest\u0026nbsp;philanthropic commitments supporting the development of AI and machine learning tools to advance mathematics. Individual grants range up to $1 million for 24 months of work on open-source projects and research.\u003C\/p\u003E","summary":"","format":"limited_html"}],"field_subtitle":"","field_summary":[{"value":"\u003Cp\u003ELeykin and his international team are developing an AI-powered interface to link proof verification and computational algebra, aiming to transform how mathematicians collaborate and solve complex problems.\u003C\/p\u003E","format":"limited_html"}],"field_summary_sentence":[{"value":"Leykin and his international team are developing an AI-powered interface to link proof verification and computational algebra, aiming to transform how mathematicians collaborate and solve complex problems."}],"uid":"36607","created_gmt":"2025-11-11 17:58:53","changed_gmt":"2025-11-12 13:10:01","author":"ls67","boilerplate_text":"","field_publication":"","field_article_url":"","location":"Atlanta, GA","dateline":{"date":"2025-11-11T00:00:00-05:00","iso_date":"2025-11-11T00:00:00-05:00","tz":"America\/New_York"},"extras":[],"hg_media":{"678593":{"id":"678593","type":"image","title":"Anton Leykin","body":"\u003Cp\u003EAnton Leykin\u003C\/p\u003E","created":"1762885000","gmt_created":"2025-11-11 18:16:40","changed":"1762885000","gmt_changed":"2025-11-11 18:16:40","alt":"man in a hat","file":{"fid":"262648","name":"GT-Anton-Leykin-Headshot-2025.png","image_path":"\/sites\/default\/files\/2025\/11\/11\/GT-Anton-Leykin-Headshot-2025.png","image_full_path":"http:\/\/hg.gatech.edu\/\/sites\/default\/files\/2025\/11\/11\/GT-Anton-Leykin-Headshot-2025.png","mime":"image\/png","size":4895966,"path_740":"http:\/\/hg.gatech.edu\/sites\/default\/files\/styles\/740xx_scale\/public\/2025\/11\/11\/GT-Anton-Leykin-Headshot-2025.png?itok=3AgS0JNU"}}},"media_ids":["678593"],"related_links":[{"url":"https:\/\/cos.gatech.edu\/news\/anton-leykin-awarded-simons-fellowship","title":"Anton Leykin Awarded Simons Fellowship"}],"groups":[{"id":"1278","name":"College of Sciences"},{"id":"1279","name":"School of Mathematics"}],"categories":[{"id":"194606","name":"Artificial Intelligence"},{"id":"135","name":"Research"}],"keywords":[{"id":"192249","name":"cos-community"},{"id":"173647","name":"_for_math_site_"},{"id":"193733","name":"_for_math_site_manual_feed_"}],"core_research_areas":[{"id":"193655","name":"Artificial Intelligence at Georgia Tech"}],"news_room_topics":[],"event_categories":[],"invited_audience":[],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003ELaura Segraves Smith, writer\u003C\/p\u003E","format":"limited_html"}],"email":["laura.smith@cos.gatech.edu"],"slides":[],"orientation":[],"userdata":""}}}