| 8:30-9:00 |
- |
Coffee |
- |
- |
| 9:00-9:45 |
I. Beloshapka |
AI for Mathematical Reasoning: Formal vs. Natural Language Approaches |
▼ |
Link |
Abstract
This talk will explore two distinct approaches to training models for mathematical problem-solving: one leveraging formal systems such as Lean, and a purely natural language-based approach. I will delve into key aspects of reinforcement learning relevant to these models and the basics of the transformer architecture. We will also explore the algorithms driving AlphaProof, an International Mathematical Olympiad silver medalist, and discuss auto-formalization.
|
| 9:50-10:35 |
H. Kera |
AI for Symbolic Computation - via Symbolic Computation |
▼ |
Link |
Abstract
The focus is on AI-assisted symbolic computation, rather than AI-assisted proving. Alongside an overview of recent studies, I will highlight open challenges that algebraists can engage with—either through collaboration with machine learning researchers or through independent contributions. In particular, I will walk through a deep learning-based approach to computing zero-dimensional ideals, where new algebraic problems naturally arise in the process of dataset generation—an essential step in training deep learning models.
|
| 10:45-11:30 |
S. Gukov |
Math + AI = AGI |
▼ |
Link |
Abstract
It comes as no surprise that solving challenging research-level math problems drives progress in mathematics. What is more surprising, though, is that solving such long-standing open problems also contributes to an entirely different field: the development of the next generation AI systems. We live in an exciting time where mathematics and AI can greatly benefit each other, and the goal of the talk is to explain how and why, drawing on specific examples from knot theory and combinatorial group theory. Largely based on recent work with Ali Shehper, Anibal Medina-Mardones, Lucas Fagan, Bart?omiej Lewandowski, Angus Gruen, Yang Qiu, Piotr Kucharski, and Zhenghan Wang.
|
| 11:35-12:20 |
A. Venkatesh |
What do we want out of proofs? |
▼ |
Link |
Abstract
I will compare two proofs of a classical result, as a means to probe what we want out of mathematical arguments. I will explain why I think this type of discussion is important in the context of AI.
|
| 12:30-13:30 |
- |
Lunch (Babbio 104) |
- |
- |
| 13:30-13:55 |
E. Bunina |
Teaching "AI in Mathematics": Designing and Delivering an Experimental Course for Mathematicians |
▼ |
Link |
Abstract
This talk presents the experience of designing and teaching an experimental course on "AI in Mathematics" for advanced undergraduate and graduate students at Stevens Institute of Technology and Bar-Ilan University. The course aimed to bridge the gap between modern AI techniques and mathematical problem-solving, focusing on real mathematical content rather than generic AI applications.
|
| 14:00-14:30 |
A. Miasnikov |
AI in Math and Math Education Lab at Stevens: thoughts, plans, and dreams |
▼ |
Link |
Abstract
Abstract will be available soon.
|
| 14:35-15:20 |
V. Stepanov |
AI In Math Education – Practical Side |
▼ |
Link |
Abstract
This talk examines how current AI/ML advances can practically transform mathematics education. Using concrete examples from Gradarius, as well as latest and greatest AI platforms, the speaker will demonstrate real-world applications that move beyond the hype to show what's actually working in classrooms today, grounding AI promises in practical reality.
|
| 15:25-16:10 |
D. Halpern-Leistner |
On the alignment problem in mathematics |
▼ |
Link |
Abstract
Foundation models are showing rapid progress in their ability to do mathematics, which makes this an exciting time to envision how these AI models can augment and accelerate mathematics research. Many also sense that this is a perilous time in the development of AI across many domains, including mathematics. Charting the path forward requires some difficult conversations about what motivates the development of mathematics and what motivates AI research, and how to bring these various motivations into alignment. I will discuss a project to do just that, by designing a benchmark for developing models that both stretch the boundaries of automated reasoning and complete tasks that will augment the workflow of the typical working mathematician. This project has grown out of a workshop at ICERM in April 2025, "Autoformalization for the working mathematician," and is a collaboration between mathematicians and ML researchers in industry and academia.
|
| 16:15-16:40 |
A. Garreta |
Solving word equations with Reinforcement Learning and SMT solvers |
▼ |
Link |
Abstract
Abstract will be available soon.
|
| 16:50-17:50 |
Roman Chernin and Speakers |
Panel Discussion |
▼ |
Link |
Abstract
Abstract will be available soon.
|
| 18:00 |
- |
Conference Dinner Banquet, Sponsored by Nebius (The Ainsworth Hoboken) |
- |
- |
