ai4math Workshop 2026

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.

TBA

TBA

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.

TBA

TBA

AI tools and agents are reshaping how researchers work, from proving theorems to training neural networks. Yet for many, it remains unclear how these tools fit into everyday research practice. This paper is a practical guide to AI-assisted research in mathematics and machine learning: We discuss how researchers can use modern AI systems productively, where these systems help most, and what kinds of guardrails are needed to use them responsibly. It is organized into three parts: (I) a five-level taxonomy of AI integration, (II) an open-source framework that, through a set of methodological rules formulated as agent prompts, turns CLI coding agents (e.g., Claude Code, Codex CLI, OpenCode) into autonomous research assistants, and (III) case studies from deep learning and mathematics. The framework runs inside a sandboxed container, works with any frontier LLM through existing CLI agents, is simple enough to install and use within minutes, and scales from personal-laptop prototyping to multi-node, multi-GPU experimentation across compute clusters. In practice, our longest autonomous session ran for over 20 hours, dispatching independent experiments across multiple nodes without human intervention. We stress that our framework is not intended to replace the researcher in the loop, but to augment them.