Loading...
Organizing Committee
University of Washington
Cornell University
University of Cambridge
Lean Focused Research Organization
Carnegie Mellon University
Abstract
A large community of pure mathematicians has recognized the importance of formal verification in modern mathematics and is looking forward to systems like Lean becoming an everyday tool in research. At the same time, automated theorem proving has recently become popular in the machine learning community as a benchmark and stepping stone for the more general task of automated reasoning. The goal of this workshop is to bring these communities together.
We will have talks and tutorials that introduce mathematicians to Lean and to state-of-the-art technologies in automated theorem proving. We will also discuss future research directions, tooling, and other ways to make this technology more useful to working mathematicians. Our medium-term goal is to initiate an effort in the mathematical community to develop a well-aligned dataset that can be used to benchmark models for tasks that are close to the use cases of working mathematicians. The first afternoon of the workshop will be a hackathon whose goal is to create tools that will aid mathematicians in this dataset creation.
We will have talks and tutorials that introduce mathematicians to Lean and to state-of-the-art technologies in automated theorem proving. We will also discuss future research directions, tooling, and other ways to make this technology more useful to working mathematicians. Our medium-term goal is to initiate an effort in the mathematical community to develop a well-aligned dataset that can be used to benchmark models for tasks that are close to the use cases of working mathematicians. The first afternoon of the workshop will be a hackathon whose goal is to create tools that will aid mathematicians in this dataset creation.
Loading...
Loading participant list in background...
Workshop Schedule
Thursday, April 24, 2025
1:20 - 1:30 PM EDT
Welcome
11th Floor Lecture Hall
Misha Kilmer, Tufts University
1:30 - 3:30 PM EDT
Hack-a-thon
Other - 11th Floor Lecture Hall
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
4:00 - 6:30 PM EDT
Hack-a-thon
Other - 11th Floor Lecture Hall
Friday, April 25, 2025
9:00 - 9:45 AM EDT
Proof Discovery as Monte Carlo Tree Search
Tutorial - 11th Floor Lecture Hall
Speaker
Leni Aniva, Stanford University
Session Chair
Kim Morrison, Lean Focused Research Organization
Abstract
In a proof assistant such as Lean, tactics incrementally evolve an incomplete proof until it becomes complete. This builds a search tree. In this talk, I will discuss the tree search formulation of proofs and how this paradigm fails. I will also explain formalizing motivated proofs and the difference between the presentation, search, and kernel views. There will be a demo of using PyPantograph to emulate this search process.
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
Preparing for the next stage in autoformalization
11th Floor Lecture Hall
Speaker
Jason Rute, Mistral AI
Session Chair
Kim Morrison, Lean Focused Research Organization
Abstract
We can’t predict what will happen in AI for math, but we can prepare. Assuming steady progress in capabilities, we could soon see AI that can autoformalize entire mathematical arguments or papers, and AI which can solve previously open mathematical problems. How do we prepare, including recording and benchmark such capabilities? In this talk I will outline my thoughts on why autoformalization is more relevant than ever and propose two specific ways can measure progress. One is a benchmark of easy-to-check autoformalizations of proofs. The other is a public repository of formalized open problems.
11:30 AM - 12:15 PM EDT
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
Tutorial - Virtual
Virtual Speaker
Jia Li, Numina
Session Chair
Kim Morrison, Lean Focused Research Organization
Abstract
We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview release. Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation by employing a structured reasoning pattern we term \textit{formal reasoning pattern}. This approach allows the model to emulate human problem-solving strategies in Lean, iteratively generating and refining proof steps. Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192. Beyond improved benchmark performance, our work yields several key insights: (1) Kimina-Prover exhibits high sample efficiency, delivering strong results even with minimal sampling (pass@1) and scaling effectively with computational budget, stemming from its unique reasoning pattern and RL training; (2) we demonstrate clear performance scaling with model size, a trend previously unobserved for neural theorem provers in formal mathematics; (3) the learned reasoning style, distinct from traditional search algorithms, shows potential to bridge the gap between formal verification and informal mathematical intuition. We open source distilled versions with 1.5B and 7B parameters of Kimina-Prover
12:25 - 12:30 PM EDT
Group Photo (Immediately After Talk)
11th Floor Lecture Hall
12:30 - 2:00 PM EDT
Lunch/Free Time
2:00 - 3:30 PM EDT
What do mathematicians (realistically) want from AI tooling?
Panel Discussion - 11th Floor Lecture Hall
Session Chair
Daniel Halpern-Leistner, Cornell University
Panelist
Alex Kontorovich, Rutgers University
Panelist
Heather Macbeth, Imperial College London
Panelist
Adam Topaz, University of Alberta
Abstract
There is a wide range of speculation about how AI is likely to affect math research. This panel will focus on the ways that working mathematicians hope to integrate AI into their research. What kind of technology would be most impactful? What technologies in AI do mathematicians see that could translate into transformative tools for research?
3:30 - 4:00 PM EDT
Coffee Break
11th Floor Collaborative Space
4:00 - 4:45 PM EDT
The SorryDB project
Tutorial - 11th Floor Lecture Hall
Speaker
Lenny Taelman, University of Amsterdam
Session Chair
Daniel Halpern-Leistner, Cornell University
Abstract
This talk reports on work-in-progress to build a continuously updating database of uncompleted ('sorry') proofs in public repositories. The aim is for this to form the basis for a continuous competition between automated provers. We intend to provide all tools necessary to make it as easy as possible to add new provers, and to make it as easy as possible for successful provers to be adopted in the real world.
5:00 - 6:30 PM EDT
Reception
11th Floor Collaborative Space
Saturday, April 26, 2025
9:00 - 9:45 AM EDT
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification
Tutorial - 11th Floor Lecture Hall
Speaker
Kaiyu Yang, Meta FAIR
Session Chair
Jarod Alper, University of Washington
Abstract
AI for Mathematics (AI4Math) is intellectually intriguing and crucial for AI-driven system design and verification. Much of the recent progress in this field has paralleled advances in natural language processing, especially by training large language models on curated mathematical text datasets. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as Lean, which can verify the correctness of reasoning and provide automatic feedback. This talk introduces the basics of AI for formal mathematical reasoning, focusing on two central tasks: theorem proving (generating formal proofs given theorem statements) and autoformalization (translating from informal to formal). I will highlight the unique challenges of these tasks through two recent projects: one on proving inequality problems from mathematics olympiads, and another on autoformalizing Euclidean geometry problems.
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 AM - 12:00 PM EDT
How hard is formalization anyway? Lessons from human formalization.
Panel Discussion - 11th Floor Lecture Hall
Session Chair
Jarod Alper, University of Washington
Panelist
Jeremy Avigad, Carnegie Mellon University
Panelist
Matthew Ballard, University of South Carolina
Panelist
Mario Carneiro, Chalmers University of Technology
Panelist
Robert Lewis, Brown University
Abstract
There is a thriving community effort to formalize mathematics, with many impressive achievements. This panel will focus on the experiences of people who have been active in this effort, and what these experiences can tell us about autoformalization. What are the main stumbling blocks that lie ahead in large scale efforts to formalize mathematics using AI? What are the most promising approaches to integrating AI into formalization efforts?
12:00 - 1:30 PM EDT
Lunch/Free Time
1:30 - 3:00 PM EDT
Industry tooling available for mathematicians over the next year?
Panel Discussion - 11th Floor Lecture Hall
Session Chair
Kim Morrison, Lean Focused Research Organization
Panelist
Jesse Michael Han, Morph
Panelist
Carina Hong, Stanford University
Panelist
Alex Meiburg, Harmonic
Panelist
Oliver Nash, N/A
Panelist
Jason Rute, Mistral AI
Abstract
Private AI labs are playing a large role in developing AI for mathematics. This panel will discuss some of the efforts in this area. What are the capabilities of current models that have yet to be deployed in tools for working mathematicians? What are the directions of research in private labs that have the potential to make an impact on mathematical research in the near term?
3:00 - 3:30 PM EDT
Coffee Break
11th Floor Collaborative Space
3:30 - 4:15 PM EDT
Verified Mathematical Reasoning with Lean and Language Models
11th Floor Lecture Hall
Speaker
Robert Joseph George, Caltech
Session Chair
Kim Morrison, Lean Focused Research Organization
Abstract
This talk will present an overview of our lab's research at the intersection of artificial intelligence and formal mathematics using the Lean theorem prover. I will discuss our foundational projects including LeanDojo, Lean Copilot, and LeanAgent, which collectively establish a framework for making formal verification more accessible to working mathematicians through AI assistance. Beyond these core systems, I will highlight several specialized applications, including our work on autoformalization of Euclidean geometry, proof progress prediction, and emerging efforts to apply Lean verification to scientific domains. Our broader goal is to extend the power of formal verification beyond pure mathematics into AI4Science applications, such as verifying solutions to partial differential equations and ensuring correctness in scientific computing. By bridging traditional mathematical practice with formal verification through AI assistance, our work aims to enhance both the accessibility and reliability of mathematical reasoning across disciplines.
4:30 - 5:15 PM EDT
From Lean to Natural Language and Back: Interfaces for Formal Proofs
11th Floor Lecture Hall
Speaker
Kyle Miller, University of California, Santa Cruz
Session Chair
Kim Morrison, Lean Focused Research Organization
Abstract
Proofs are written to persuade skeptics—once only human readers, and now also machines. But humans and machines have different needs. What if we want to satisfy both? In this talk, I’ll present two directions for bridging this gap. LeanInformal automatically translates Lean proofs into interactive documents with readable English using classical NLP techniques. Verbose Lean, developed by Patrick Massot for use in education, is a library for writing Lean proofs in a controlled natural language. I’ll situate these tools in the broader landscape of using natural language as an interface to mathematics and explore how they might help humans and machines build theory together. This is joint work with Patrick Massot.
Sunday, April 27, 2025
9:00 - 9:45 AM EDT
TBA
Tutorial - 11th Floor Lecture Hall
Speaker
Jesse Michael Han, Morph
Session Chair
Daniel Halpern-Leistner, Cornell University
10:00 - 10:30 AM EDT
Coffee Break
11th Floor Collaborative Space
10:30 - 11:15 AM EDT
Proofs and the tools they use
11th Floor Lecture Hall
Speaker
Heather Macbeth, Imperial College London
Session Chair
Daniel Halpern-Leistner, Cornell University
Request Reimbursement
This section is for general purposes only and does not indicate that all attendees receive funding. Please refer to your personalized invitation to review your offer.
- ORCID iD
- As this program is funded by the National Science Foundation (NSF), ICERM is required to collect your ORCID iD if you are receiving funding to attend this program. Be sure to add your ORCID iD to your Cube profile as soon as possible to avoid delaying your reimbursement.
- Acceptable Costs
- 1 roundtrip between your home institute and ICERM
- Flights in economy class to either Providence airport (PVD) or Boston airport (BOS)
- Ground Transportation to and from airports and ICERM.
- Unacceptable Costs
- Flights on U.K. airlines
- Seats in economy plus, business class, or first class
- Change ticket fees of any kind
- Multi-use bus passes
- Meals or incidentals
- Advance Approval Required
- Personal car travel to ICERM from outside New England
- Multiple-destination plane ticket; does not include layovers to reach ICERM
- Arriving or departing from ICERM more than a day before or day after the program
- Multiple trips to ICERM
- Rental car to/from ICERM
- Arriving or departing from airport other than PVD/BOS or home institution’s local airport
- 2 one-way plane tickets to create a roundtrip (often purchased from Expedia, Orbitz, etc.)
- Travel Maximum Contributions
- New England: $350
- Other contiguous US: $850
- Asia & Oceania: $2,000
- All other locations: $1,500
- Note these rates were updated in Spring 2023 and supersede any prior invitation rates.
- Reimbursement Requests
Request Reimbursement with Cube
Refer to the back of your ID badge for more information. Checklists are available at the front desk and in the Reimbursement section of Cube.
- Reimbursement Tips
- Scanned original receipts are required for all expenses
- Airfare receipt must show full itinerary and payment
- ICERM does not offer per diem or meal reimbursement
- Allowable mileage is reimbursed at prevailing IRS Business Rate and trip documented via Google Maps PDF
- Keep all documentation until you receive your reimbursement!
- Reimbursement Timing
6–8 weeks after all documentation is sent to ICERM. All reimbursements are reviewed by multiple Brown University offices.
- Reimbursement Deadline
Submissions must be received within 30 days of ICERM departure to avoid applicable taxes. No submissions are accepted after six months.