Home

Welcome to

2nd AI for Math Workshop @ ICML 2025

https://icml.cc/virtual/2025/workshop/39979

Ballroom C, West Building, Vancouver Convention Center

July 18th, 2025 @ Vancouver, Canada (Hybrid).

HISTORY OF AI FOR MATH WORKSHOP

AI for Math Workshop @ ICML 2024

WORKSHOP SUMMARY

Mathematical reasoning stands as a pinnacle of human intelligence. The rapid advancements in artificial intelligence, particularly in large language models (LLMs), have opened new frontiers at the intersection of AI and mathematical reasoning. This workshop aims to explore the potential of AI in comprehending and advancing mathematical reasoning, with a focus on fostering collaboration between humans and machines to push the boundaries of mathematical discovery. The central theme revolves around the question:

“How can we leverage and advance the mathematical reasoning abilities of machine learning models, and drive innovation across scientific and practical domains?”

Our workshop will bring together researchers from diverse backgrounds, institutions, and disciplines to discuss the progress and future of AI technologies in mathematics. Specifically, we will delve into the areas related to the following:

Automated Theorem Proving: How can we build consistent theorem-proving systems? How can theorem-proving systems assist humans through human-computer interaction?
Automated Theorem Generation: Can neural models generate new and practically meaningful theorems that have been discovered? How can we utilize these newly generated theorems?
Autoformalization and Verification: How can we improve the precision of translating natural language proofs into formal proofs, and vice versa?
Problem Solving: How can we develop AI models to solve complex mathematical computational problems across various domains? How can AI models improve themselves during the learning process?
Applications of AI in Mathematics: What are the practical applications of AI-driven mathematical reasoning in various fields such as sciences, engineering, finance, and education?

The intended outcome is to identify new ideas, open problems, and interdisciplinary areas for future research related to mathematical reasoning. To this end, we welcome papers on areas related, but not limited, to:

Algorithm: How to develop effective algorithms (e.g., reinforcement learning, self-improve/evolve) to improve reasoning ability? What are the key principles for developing algorithms that minimize resource consumption (e.g., time, memory) while maintaining or improving reasoning performance?
Data Generation: Can AI models generate questions that they cannot answer correctly? Can AI models achieve self-improvement through self-generated data?
Tool Utilization: How can AI systems leverage existing tools, such as code and software, to solve practical mathematical problems more effectively?
Limitation Analysis: What are the drawbacks or limitations of current models in mathematical reasoning (e.g., robustness, generalization, and reasoning boundary)? How can these limitations be quantitatively analyzed?

INVITED SPEAKERS & PANELISTS

Swarat Chaudhuri

Swarat Chaudhuri is a Professor of Computer Science and the director of the Trishul laboratory at UT Austin. His research lies at the interface of programming languages, formal methods, and machine learning. His aim as a researcher is to develop a new class of intelligent systems that are reliable, transparent, and secure by construction and can solve reasoning-intensive tasks beyond the scope of contemporary AI. He has received the NSF CAREER award, the ACM SIGPLAN John Reynolds Dissertation award, the Morris and Dorothy Rubinoff Dissertation award from the University of Pennsylvania, Meta and Google Research awards, and several ACM SIGPLAN and SIGSOFT distinguished paper awards.

Hannaneh Hajishirzi

Hanna Hajishirzi is the Torode Family Associate Professor in the Allen School of Computer Science and Engineering at the University of Washington and a Senior Director of NLP at AI2. She received her Ph.D in Computer Science from University of Illinois at Urbana-Champaign, and spent a year as Postdoctoral associate at Disney Research and CMU. Her current research delves into various areas within NLP and AI, with a particular focus on understanding and pushing the boundaries of large language models. She has published more than 140 scientific articles in top-tier journals and conferences in ML, AI, NLP, and Computer Vision. She is a recipient of 2020 Alfred Sloan Fellowship, 2021 NSF CAREER award, 2019 Intel rising star award, 2018 Allen Distinguished Investigator award, 2023 Academic Achievement UIUC Alumni award, 2024 innovator of the year award finalist by GeekWire, and several research faculty awards from industry. The work from her lab has been nominated or received best paper awards at conferences and have been featured in a variety of magazines and newspapers including New York Times, Forbes, NPR, MIT Technology Review, Geekwire, Wired Magazine, and more.

Jeremy Avigad

Jeremy Avigad is a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University. He is a mathematical logician and philosopher of mathematics who uses logical methods to understand mathematical language, mathematical proof, and the principles of mathematical reasoning.

Huajian Xin

Huajian Xin is currently a PhD student at the University of Edinburgh, supervised by Dr. Wenda Li, and is concurrently interning with the Seed team at ByteDance. His research focuses on automated theorem proving using large language models within formal mathematical environments. He specializes in autonomous agents capable of autoformalization and knowledge library learning, striving to advance deep integration and synergy between large language models and formal systems. His representative works include the leading open-source theorem proving model series DeepSeek Prover, and lemma decomposition and knowledge accumulation system LEGO-Prover, and proof engineering benchmark APE-Bench.

Amaury Hayat

Amaury Hayat is a full professor at Ecole des Ponts ParisTech in France, where he has been a faculty member since 2019. His research interests include control theory, partial differential equations, and AI for mathematics.

Mrinmaya Sachan

Mrinmaya Sachan is an Assistant Professor in the Department of Computer Science at ETH Zurich. He received his PhD from Carnegie Mellon University. His research spans natural language processing, knowledge representation and reasoning. He is also interested in problems in the intersection of NLP and Education.. He received an outstanding paper award at ACL 2015, multiple fellowships (IBM and Facebook fellowships, Siebel scholarship and CMU CMLH fellowship) during his PhD. His research group is supported by the Swiss National Science Foundation, ETH Zurich and Haslerstiftung.

Moa Johansson

Moa Johansson is currently an Associate Professor (Docent) at Chalmers University. Her research interests include a diverse mix of applications of AI: from mathematics and automated reasoning to sports science and natural language processing for political science.

Leonardo de Moura

Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.