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

PROGRAM SCHEDULE

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

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.

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.

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.

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.

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.

Valentina Pyatkin

Valentina is a postdoctoral researcher (and Young Investigator) at the Allen Institute for AI and the University of Washington, advised by Prof. Yejin Choi and Prof. Hanna Hajishirzi. She completed my PhD in Computer Science at the NLP lab of Bar Ilan University, supervised by Prof. Ido Dagan and Prof. Reut Tsarfaty. She also was a visiting PhD student at UW NLP and interned twice at the Allen Institute for AI. Her work has been awarded an ACL Outstanding Paper Award and the ACL Best Theme Paper Award. She has received the AI2 Outstanding Intern of the Year Award. Previously she did a research internship at Google, obtained an MSc from the University of Edinburgh and a BA from the University of Zurich. Her work has been featured in the press, for example by TechCrunch and GeekWire.

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.

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.

Sergei Gukov

Sergei is a professor of mathematics and theoretical physics at Caltech. He is renowned for his work at the interface of geometry, quantum field theory, and number theory, and is one of the pioneers harnessing and developing reinforcement learning methods for knot theory and combinatorial group theory.