Proving Theorems with Lean and Machine Learning
Proving Theorems with Lean and Machine Learning
ICML 2026 Tutorial
July 6, 2026 -- Seoul, South Korea
ICML Event Page
Lean Website
Lean Zulip
Lean Community (Mathlib)
Abstract
AI agents can now write mathematics, including proofs of theorems relevant to Machine Learning, but we can’t trust them yet. Subtle errors might be hidden deep in the reasoning steps, and checking the proofs manually takes a lot of time and expertise. The Lean theorem prover provides a way to write formal, machine-checkable proofs, giving us high confidence in their correctness. AI systems have managed to reach gold medal level at the International Mathematical Olympiad while producing Lean-checked proofs. Could we get them to write research-level, verified mathematics?
In this tutorial, we introduce Lean and its mathematical library Mathlib, and show how they can be used to write trusted proofs, in particular machine learning theory proofs. We then show how machine learning can help with theorem proving, and present recent advances in AI-assisted formalization.
Speakers
Learning Resources
Lean and Mathlib
-
Lean website, with installation instructions
-
The Natural Number Game, a fun in-browser game to learn Lean
-
Glimpse of Lean, an interactive tutorial for mathematics in Lean
AI for Theorem Proving
-
Lean-lsp-mcp, to give your AI agent access to Lean functionality
-
Lean 4 Skills, skill files for mathematics in Lean
Lean Machine Learning
-
The Lean Machine Learning project aims to provide a library of formal definitions for machine learning theory in Lean. The project is open-source and welcomes contributions from the community.
-
There will be a workshop on formalizing machine learning in Lean, with AI. December 2026 in Lille, France.
Sponsor
We are grateful for the support of ICARM, the Institute for Computer-Aided Reasoning in Mathematics, an NSF Mathematical Sciences Institute.
