The ai4math Workshop 2026 is the first workshop of the ai4math Berlin-Brandenburg network. It brings together researchers interested in the use of artificial intelligence as a tool for mathematical research.
Our focus is on AI for mathematics rather than the mathematical analysis of AI systems. Topics of interest include large language models, automated and interactive theorem proving, proof assistants, formal verification, mathematical knowledge management, conjecture generation, proof discovery, symbolic methods, and related approaches.
The workshop aims to strengthen the emerging AI-for-mathematics community in the Berlin-Brandenburg region and beyond. In particular, we want to:
connect researchers from mathematics, computer science, and AI,
showcase current work and ongoing projects,
discuss opportunities for collaboration,
identify common infrastructure and research needs,
grow the ai4math network and welcome new participants.
Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. In this lecture, we present an approach to computer theorem proving that employs specialized language models for Lean4 proof generation combined with recursive decomposition of difficult theorems into simpler entailing propositions. We will discuss how these models are coordinated through a multi-agent architecture that orchestrates autoformalization, proof generation, decomposition, and recursive proving. Additionally, we will highlight a key technical contribution: our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities to facilitate automated, recursive proof decomposition. Finally, we will introduce the open-source implementation available on PyPI as “goedels-poetry” and on GitHub at https://github.com/KellyJDavis/goedels-poetry, demonstrating how it facilitates adaptation to alternative language models and custom extensions.
Generative learning has the potential to reshape engineering and applied mathematics, from numerical solutions of PDE, solution to inverse problems to generative design, where the customer creates a design interacting with a generative model. An overview is given about recent technical progress and the mathematical structures that stand behind it.
After a minimal introduction to Lean’s type theory and its use for proof checking, we’ll present recent work on heuristic proof search tactics in the line of Aesop.
We’ll discuss approaches to forward & backward proof search, aspects of rewriting, and most importantly, a heuristic for search step selection based on a generalization proceedure on proof state data.
Along the way, we’ll discuss two key data structures, set-tries and path indices, as well as proof state sampling from elaborated proof terms.
Teaching how AI can help in mathematical research is about more than clever prompts. It is about understanding the structure of mathematical progress and a general effective use of computational tools.
I give an overview of a course that I have taught in different variants. I show how one can use the curiosity about the latest AI advances for a deeper understanding of the structure of mathematics.
In this talk, we first analyze the challenges of contemporary university mathematics education and how AI is affecting them. We then discuss the role of AI in teaching mathematics, outline concrete use cases, and propose a new perspective on the traditional components of university mathematics education in light of AI.
Martin Raum (Chalmers University of Technology, Göteborg)#
Title: AI is a tool: A working mathematician’s experience and perspective
I trace how AI entered my research workflow and how I refined the surrounding tools. I focus on two aspects in particular: manuscript review and infrastructure. AI has become a useful component of my toolchain, while mathematical judgment remains with me, the researcher.
I will present my ongoing Master Thesis about formalizing
aspects of Hyperbolic Geometry in Lean. I will share my experience and
the challenges I had with Lean and Mathlib. I will also mention how AI
has helped me (or not).
Title: Text-Diffusion Models for Mathematical Reasoning
Abstract
Diffusion language models generate in parallel and can revise themselves, which makes them an appealing basis for mathematical reasoning. I’ll talk about general generation paradigms (Autoregressive, Masked diffusion & Continuous diffusion), my experiences from training a 1.2B Masked diffusion proofer, and why a tuned sudoku puzzle may be the ideal proxy problem for Lean proofs (including training results).
Pruning—the removal of parameters from neural networks—is a standard technique for reducing the inference cost and memory requirements of large language models. This talk presents two efficient
approaches to the underlying mask-selection problem: SparseSwaps, which refines pruning masks through
pairwise weight exchanges, and SparseFW, which relaxes the combinatorial problem and optimizes it
using the Frank–Wolfe algorithm. While both methods substantially reduce layer-wise reconstruction error, their development also exposes a broader issue: improving the local pruning objective does not necessarily improve the full model. We then show how an agentic research workflow helped uncover a systematic decay in pruned model outputs and led to a simple magnitude correction with strong empirical improvements. Beyond the pruning results, the talk discusses practical lessons for turning general-purpose coding agents into effective research collaborators through structured instructions, explicit safeguards, and reproducible workflows.
The ai4math Berlin-Brandenburg network brings together researchers interested in the use of AI for mathematical research. The network aims to foster collaboration, exchange ideas, and build a strong regional and international community around AI-assisted mathematics.
