Lean and ML

Proving Theorems with Lean and Machine Learning

Rémy Degenne Univ. Lille, Inria, CNRS, Centrale Lille, CRIStAL; Mathlib maintainer

Wenda Li University of Edinburgh

Université de Lille

Inria

University of Edinburgh

With support from

ICARM

This tutorial

Proving (machine learning) theorems with Lean
Machine learning for theorem proving

https://leanmachinelearning.org/icml-tutorial/

Lean is a proof assistant

A programming language in which you can write theorems and proofs.

A compiler that checks that your proofs are correct.

2024

Deepmind silver medal, IMO 2024

with Lean proofs

2025

Harmonic gold medal, IMO 2025

Lean

OpenAI gold medal, IMO 2026

No Lean

2026

Aletheia first proof, 2026

OpenAI Erdős

Now with Lean proof

The challenge

Aletheia Erdős, 2026

https://www.erdosproblems.com/ by Thomas Bloom

Human grading, expert mathematicians are expensive.

A functional programming language

def helloWorld : IO Unit := IO.println "Hello, world!"

#evalHello, world!
 helloWorld
Hello, world!

A proof assistant

variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
  [StandardBorelSpace Ω]
  {P : Measure Ω} [IsProbabilityMeasure P]
  {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ}

/-- Chernoff tail bound for sub-Gaussian random
variables. -/
example (h_adapted : StronglyAdapted ℱ X)
    (h0 : HasSubgaussianMGF (X 0) (c 0) P) (n : ℕ)
    (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (ℱ i)
      (ℱ.le i) (X (i + 1)) (c (i + 1)) P)
    {ε : ℝ} (hε : 0 ≤ ε) :
    P.real {ω | ε ≤ ∑ i ∈ range n, X i ω}
      ≤ exp (-ε ^ 2 / (2 * ∑ i ∈ range n, c i)) :=
  (HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF h_adapted
    h0 n h_subG).measure_ge_le hε

Other proof assistants: Rocq, Isabelle, HOL, Agda, Mizar...

An extensible language

Write proofs about programs.
Write programs that produce proofs.

And more: these slides are generated from a Lean file!

Formal mathematics with Lean

You want to prove a theorem in Lean

You import some results you need from a library
You write a statement in the Lean language
You write a proof, using tactics (programs)
The Lean kernel checks that your proof is correct

Now your theorem can be used in other proofs, locally.

Next step: you add your result to a library

Notable projects in formal mathematics

Before Lean, before AI.

2005: Four colour theorem (Rocq)
2012: Odd Order Theorem (Rocq)
2014 Kepler's conjecture (Isabelle/HOL Light)

Liquid Tensor Experiment

Challenge by Peter Scholze, 2020

LTE Challenge

Completed in 2022. Johan Commelin, Adam Topaz,

Reid Barton, Alex J. Best, Riccardo Brasca, Kevin Buzzard, Yaël Dillies, Floris van Doorn, Fabian Glöckle, Markus Himmel, Heather Macbeth, Patrick Massot, Bhavik Mehta, Kim Morrison, Filippo A. E. Nuccio, Joël Riou, Damiano Testa, Andrew Yang

PFR conjecture

PFR Challenge

Proved by Gowers, Green, Manners and Tao, 2023

exampledeclaration uses `sorry` {A : Set G} {K : ℝ} (h₀A : A.Nonempty)
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 12 ∧
        Nat.card H ≤ Nat.card A ∧ A ⊆ c + H :=
  sorry

Formalized, 3 weeks later.

Terence Tao, Yaël Dillies, Rémy Degenne, Sébastien Gouëzel, Kalle Kytölä, Paul Lezeau, Arend Mellendijk, Floris van Doorn, Lawrence Wu, Ben Eltschig, Kim Morrison, Utensil Song, Heather Macbeth, Mantas Bakšys, Jonas Bayer, Mauricio Collares, Patrick Massot, Kyle Miller, Kaiyu Yang, Oliver Nash, Aaron Anderson, Sky Wilshaw, Rob Lewis, Pietro Monticone, Thomas Bloom, Adam Topaz, Kevin Buzzard

CEDAR

A language for access control. Define who is authorized to do what within your application.

Cedar Analysis toolkit by AWS.

a compiler implemented in Lean translates Cedar policies into mathematical formulas.
prove properties of the policies (e.g. only users with appropriate permissions can access a resource)

SampCert

AWS's SampCert library: verifed differential privacy algorithms deployed in their Clean Rooms service.

Uses Mathlib (Lean's mathematical library), for example the Poisson summation formula.

example
    {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b)
    (hf : f =O[cocompact ℝ] fun x ↦ |x| ^ (-b))
    (hFf : (𝓕 f) =O[cocompact ℝ] fun x ↦ |x| ^ (-b))
    (x : ℝ) :
    ∑' n : ℤ, f (x + n) =
      ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) :=
  Real.tsum_eq_tsum_fourier_of_rpow_decay hc hb hf hFf x

Why formalize mathematics?

verification: check correctness, trust
understanding: search the library, explore the proof
creation: remove a hypothesis and see what breaks, find generalizations, use automation
collaboration: leverage the trust to work together

New reason: check AI output

Collaboration

25 collaborators on PFR. How?

Lean checks the proof: I don't need to know you and trust you're good at maths to believe your proof.

Blueprint

Blueprint tool by Patrick Massot

AI + formal math possibilities

You write a new proof, and write it in Lean
You write a new proof, and an AI checks it with Lean
You ask an AI to prove parts of your argument, and check it with Lean
You research a problem in conversation with an AI with Lean access
You throw money at an AI to prove your theorem, with a Lean proof

Writing proofs in Lean

variable {𝓧 : Type*} [MeasurableSpace 𝓧] {f g : 𝓧 → ℝ≥0∞}
  (hf : Measurable f) (hg : Measurable g)

example : Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  apply Measurable.add hf ?_𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun a => g a / 2
  apply Measurable.div_const ?_ 2𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable g
  exact hgAll goals completed! 🐙

example : Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  exact hf.add (hg.div_const 2)All goals completed! 🐙

example : Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  fun_propAll goals completed! 🐙

example [TopologicalSpace 𝓧] (f g : 𝓧 → ℝ)
    (hf : Continuous f) (hg : Continuous g) :
    Continuous (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝¹:MeasurableSpace 𝓧f✝:𝓧 → ℝ≥0∞g✝:𝓧 → ℝ≥0∞hf✝:Measurable f✝hg✝:Measurable g✝inst✝:TopologicalSpace 𝓧f:𝓧 → ℝg:𝓧 → ℝhf:Continuous fhg:Continuous g⊢ Continuous fun x => f x + g x / 2
  fun_propAll goals completed! 🐙

Writing proofs in Lean

lemma wrong_proof
    (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  apply Continuous.add𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2Tactic `apply` failed: could not unify the conclusion of `@Continuous.add`
  Continuous ?f → Continuous ?g → Continuous (?f + ?g)
with the goal
  Measurable fun x => f x + g x / 2

Note: The full type of `@Continuous.add` is
  ∀ {M : Type ?u.35} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type ?u.34}
    [inst_3 : TopologicalSpace X] {f g : X → M}, Continuous f → Continuous g → Continuous (f + g)

𝓧:Type u_1inst✝:MeasurableSpace 𝓧f g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2

lemma incomplete_lemmadeclaration uses `sorry`
    (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  sorryAll goals completed! 🐙

lemma sorryful_lemma
    (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun x ↦ f x + (g x / 2)) := by𝓧:Type u_1inst✝:MeasurableSpace 𝓧f:𝓧 → ℝ≥0∞g:𝓧 → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Measurable fun x => f x + g x / 2
  exact incomplete_lemma hf hgAll goals completed! 🐙

#print'sorryful_lemma' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] axioms sorryful_lemma

Lean checks the proof, reports errors, emits warnings

Definitions and theorems

/-- My favorite number. -/
def myFavoriteNumber : ℕ := 42

theorem myFavoriteNumber_eq_40_plus_2 :
    myFavoriteNumber = 40 + 2 := by⊢ myFavoriteNumber = 40 + 2
  unfold myFavoriteNumber⊢ 42 = 40 + 2
  simpAll goals completed! 🐙

theorem even_myFavoriteNumber :
    Even myFavoriteNumber := by⊢ Even myFavoriteNumber
  unfold myFavoriteNumber⊢ Even 42
  grindAll goals completed! 🐙

#checkmyFavoriteNumber : ℕ myFavoriteNumber

myFavoriteNumber : ℕ
#checkEven myFavoriteNumber : Prop Even myFavoriteNumber

Even myFavoriteNumber : Prop
#checkeven_myFavoriteNumber : Even myFavoriteNumber even_myFavoriteNumber
even_myFavoriteNumber : Even myFavoriteNumber

Wrong definitions

def IsSubGaussianProcess (μ : Measure Ω)
    (X : E → Ω → ℝ) (σ : ℝ) : Prop :=
  ∀ s t : E, ∀ l : ℝ,
    ∫ ω, exp (l * (X s ω - X t ω)) ∂μ ≤
      exp (l^2 * σ^2 * (dist s t)^2 / 2)

What if \exp(l (X_s - X_t)) is not integrable?

The integral is 0 by definition. Not what we want.

Lean checks proofs, it does not read your mind.

Lean Mathematical Ecosystem

Lean
Mathlib: mathematical library
Downstream libraries: CSLib, PhysLib, FLT, LML...

Discussions on Zulip: https://leanprover.zulipchat.com

Mathlib

A community-driven library of formalized mathematics in Lean.

open source (772 contributors)
maintained (29 maintainers), carefully reviewed (58+ reviewers)
infrastucture: CI, deprecation cycle, testing, documentation
definitions written in the right generality, applicable to many situations

definitions written in the right generality, applicable to many situations

Not merely formalized: digested, generalized, organized, reusable.

Formalized matematics in Mathlib

Mathlib contains most of an undergraduate mathematics curriculum.

Formalizing machine learning

Many prerequisites are there, in measure theory, probability theory (discrete time), functional analysis, linear algebra, optimization, ...
Everything ML-specific is missing from Mathlib
With Paulo Rauber, we formalized basic bandit algorithms and optimization proofs.
Others have auto-formalized optimization or stochastic learning theory results (like the IsSubGaussianProcess definition above).

Can I ask my LLM to do it?

Possibly, but.

The Mathlib Halo

Mathlib halo

Beyond the halo, you need a very good harness, domain knowledge and/or lots of resources for your AI to produce working code.

Cheating

/-- Totally legit prime definition. -/
def IsPrime (n : ℕ) : Prop := true

theorem twin_primes :
    {p : ℕ | IsPrime p ∧ IsPrime (p + 2)}.Infinite := by⊢ {p | IsPrime p ∧ IsPrime (p + 2)}.Infinite
  simp [IsPrime]⊢ Set.univ.Infinite
  exact Set.infinite_univAll goals completed! 🐙

#print'twin_primes' depends on axioms: [propext, Classical.choice, Quot.sound] axioms twin_primes

Cheating

Lean is extensible: you can redefine everything.

You can change Nat.Prime to always return true.
You can redefine #print axioms to hide sorry.

Your LLM can and will cheat.

A solution: use the Comparator tool.

Quality issues

restricted definition (perhaps the general one requires too much background)
too many hypotheses (need to be checked at every use)
slow, inefficient code
unmaintainable, brittle code
lack of understanding
lack of attribution

Piles of definitions

The result of 500k lines of AI formalization:

Object A has property P under assumption H.

A depends on 50 new definitions. Same for P and H.

How do you audit the definitions?

Lean Machine Learning

https://leanmachinelearning.org

A library of formalized machine learning theory definitions

/-- A stochastic, sequential algorithm. -/
structure Algorithm (𝓐 𝓨 : Type*)
    [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy: distribution of the next action. -/
  policy : (n : ℕ) → Kernel (Iic n → 𝓐 × 𝓨) 𝓐
  [h_policy : ∀ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  [hp0 : IsProbabilityMeasure p0]

Demo: online gradient descent

x_0 \in E, \eta > 0, (g_n) \in E^{\mathbb{N}}

x_{n+1} = x_n - \eta g_n

Goal:

\sum_{i=0}^{n-1} \langle x_i - y, g_i \rangle \leq \frac{1}{2\eta} \|x_0 - y\|^2 + \frac{\eta}{2} \sum_{i=0}^{n-1} \|g_i\|^2

Demo: online gradient descent

open Real Finset
open scoped RealInnerProductSpace

variable {E : Type*}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {γ : ℕ → ℝ} {η : ℝ}

lemma inner_eq_add (x y g : E) (hη : 0 < η) :
    ⟪x - y, g⟫ =
      (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖(x - η • g) - y‖ ^ 2) +
      (η / 2) * ‖g‖ ^ 2 := byE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < η⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖x - η • g - y‖ ^ 2) + η / 2 * ‖g‖ ^ 2
  have hsub : (x - η • g) - y = (x - y) - η • g := by abelAll goals completed! 🐙E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < ηhsub:x - η • g - y = x - y - η • g⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖x - η • g - y‖ ^ 2) + η / 2 * ‖g‖ ^ 2
  rw [hsub,E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < ηhsub:x - η • g - y = x - y - η • g⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - ‖x - y - η • g‖ ^ 2) + η / 2 * ‖g‖ ^ 2 norm_sub_sq_real (x - y) (η • g)E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < ηhsub:x - η • g - y = x - y - η • g⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - (‖x - y‖ ^ 2 - 2 * ⟪x - y, η • g⟫ + ‖η • g‖ ^ 2)) + η / 2 * ‖g‖ ^ 2]E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < ηhsub:x - η • g - y = x - y - η • g⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - (‖x - y‖ ^ 2 - 2 * ⟪x - y, η • g⟫ + ‖η • g‖ ^ 2)) + η / 2 * ‖g‖ ^ 2
  simp only [inner_smul_right, norm_smul, norm_eq_abs,
    abs_of_pos hη]E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:Ey:Eg:Ehη:0 < ηhsub:x - η • g - y = x - y - η • g⊢ ⟪x - y, g⟫ = (2 * η)⁻¹ * (‖x - y‖ ^ 2 - (‖x - y‖ ^ 2 - 2 * (η * ⟪x - y, g⟫) + (η * ‖g‖) ^ 2)) + η / 2 * ‖g‖ ^ 2
  fieldAll goals completed! 🐙

lemma sum_inner_le_sum' (x y g : ℕ → E) (hγ : ∀ n, 0 < γ n)
    (n : ℕ) :
    ∑ i ∈ range n, ⟪x i - y i, g i⟫ ≤
      ∑ i ∈ range n, ((2 * γ i)⁻¹ *
        (‖x i - y i‖ ^ 2 - ‖(x i - γ i • g i) - y i‖ ^ 2) +
        (γ i / 2) * ‖g i‖ ^ 2) := byE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eγ:ℕ → ℝx:ℕ → Ey:ℕ → Eg:ℕ → Ehγ:∀ (n : ℕ), 0 < γ nn:ℕ⊢ ∑ i ∈ range n, ⟪x i - y i, g i⟫ ≤
  ∑ i ∈ range n, ((2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x i - γ i • g i - y i‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2)
  gcongr with i hihE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eγ:ℕ → ℝx:ℕ → Ey:ℕ → Eg:ℕ → Ehγ:∀ (n : ℕ), 0 < γ nn:ℕi:ℕhi:i ∈ range n⊢ ⟪x i - y i, g i⟫ ≤ (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x i - γ i • g i - y i‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2
  rw [inner_eq_add (x i) (y i) (g i) (hγ i)hE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eγ:ℕ → ℝx:ℕ → Ey:ℕ → Eg:ℕ → Ehγ:∀ (n : ℕ), 0 < γ nn:ℕi:ℕhi:i ∈ range n⊢ (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x i - γ i • g i - y i‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2 ≤
  (2 * γ i)⁻¹ * (‖x i - y i‖ ^ 2 - ‖x i - γ i • g i - y i‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2]All goals completed! 🐙

lemma sum_inner_le_sum (x g : ℕ → E) (y : E)
    (hγ : ∀ n, 0 < γ n)
    (hx : ∀ n, x (n + 1) = x n - γ n • g n) (n : ℕ) :
    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
      ∑ i ∈ range n, ((2 * γ i)⁻¹ *
        (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) +
        (γ i / 2) * ‖g i‖ ^ 2) :=
  (sum_inner_le_sum' x (fun _ ↦ y) g hγ n).trans_eq
    (byE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eγ:ℕ → ℝx:ℕ → Eg:ℕ → Ey:Ehγ:∀ (n : ℕ), 0 < γ nhx:∀ (n : ℕ), x (n + 1) = x n - γ n • g nn:ℕ⊢ ∑ i ∈ range n, ((2 * γ i)⁻¹ * (‖x i - y‖ ^ 2 - ‖x i - γ i • g i - y‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2) =
  ∑ i ∈ range n, ((2 * γ i)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + γ i / 2 * ‖g i‖ ^ 2) simp [hx]All goals completed! 🐙)

section ConstantStep

lemma sum_inner_le_add (x g : ℕ → E) (y : E)
    (hη : 0 < η) (hx : ∀ n, x (n + 1) = x n - η • g n)
    (n : ℕ) :
    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
      (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) +
      (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := byE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤ (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2
  refine (sum_inner_le_sum x g y
    (fun _ ↦ hη) hx n).trans_eq ?_E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ ∑ i ∈ range n, ((2 * η)⁻¹ * (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + η / 2 * ‖g i‖ ^ 2) =
  (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2
  rw [sum_add_distrib,E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ ∑ x_1 ∈ range n, (2 * η)⁻¹ * (‖x x_1 - y‖ ^ 2 - ‖x (x_1 + 1) - y‖ ^ 2) + ∑ x ∈ range n, η / 2 * ‖g x‖ ^ 2 =
  (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 ← mul_sum,E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ (2 * η)⁻¹ * ∑ i ∈ range n, (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + ∑ x ∈ range n, η / 2 * ‖g x‖ ^ 2 =
  (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 ← mul_sum,E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ (2 * η)⁻¹ * ∑ i ∈ range n, (‖x i - y‖ ^ 2 - ‖x (i + 1) - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 =
  (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2
    sum_range_sub' (fun i ↦ ‖x i - y‖ ^ 2) nE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Eη:ℝx:ℕ → Eg:ℕ → Ey:Ehη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 =
  (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2]All goals completed! 🐙

/-- Regret bound for gradient descent and linear losses. -/
lemma regret_bound (x g : ℕ → E) (y : E) (η : ℝ)
    (hη : 0 < η) (hx : ∀ n, x (n + 1) = x n - η • g n)
    (n : ℕ) :
    ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤
      (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 +
      (η / 2) * ∑ i ∈ range n, ‖g i‖ ^ 2 := byE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:ℕ → Eg:ℕ → Ey:Eη:ℝhη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ ∑ i ∈ range n, ⟪x i - y, g i⟫ ≤ (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2
  grw [sum_inner_le_add x g y hη hx nE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:ℕ → Eg:ℕ → Ey:Eη:ℝhη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 ≤
  (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2]E:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:ℕ → Eg:ℕ → Ey:Eη:ℝhη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ (2 * η)⁻¹ * (‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2) + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2 ≤
  (2 * η)⁻¹ * ‖x 0 - y‖ ^ 2 + η / 2 * ∑ i ∈ range n, ‖g i‖ ^ 2
  gcongrhbcE:Type u_4inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:ℕ → Eg:ℕ → Ey:Eη:ℝhη:0 < ηhx:∀ (n : ℕ), x (n + 1) = x n - η • g nn:ℕ⊢ ‖x 0 - y‖ ^ 2 - ‖x n - y‖ ^ 2 ≤ ‖x 0 - y‖ ^ 2
  exact sub_le_self _ (sq_nonneg _)All goals completed! 🐙

end ConstantStep

proving vs understanding

The product of mathematics is clarity and understanding. Not theorems, by themselves.

William Thurston

We are transitioning in mathematics from an era of proof scarcity to an era of proof abundance, but our mathematical infrastructure and culture has not yet adapted to this. As mentioned previously, there is now a strong (and growing) impedance mismatch between the three core components of mathematical problem solving: proof generation, proof verification, and proof digestion.

Terence Tao

There is value in formalizing quickly to be able to check research results
There is value in carefully designing a library to be able to further our understanding

Questions?

Formal mathematics is ready for large scale adoption.

https://leanmachinelearning.org/workshop/

Proving Theorems with Lean and Machine Learning

This tutorial

Lean is a proof assistant

2024

2025

2026

The challenge

​

A functional programming language

A proof assistant

An extensible language

Formal mathematics with Lean

Notable projects in formal mathematics

Liquid Tensor Experiment

PFR conjecture

CEDAR

SampCert

Why formalize mathematics?

Collaboration

AI + formal math possibilities

Writing proofs in Lean

Writing proofs in Lean

Definitions and theorems

Wrong definitions

Lean Mathematical Ecosystem

Mathlib

Formalized matematics in Mathlib

​

Formalizing machine learning

Can I ask my LLM to do it?

The Mathlib Halo

Cheating

Cheating

Quality issues

Piles of definitions

Lean Machine Learning

Demo: online gradient descent

Demo: online gradient descent

proving vs understanding

Questions?