Around Formalization: Why and How to Explain Mathematics to a Computer

Riccardo Brasca
Institut de Mathématiques de Jussieu-Paris Rive Gauche
Université Paris Cité

Colloquia Patavina | Università di Padova | May 5, 2026

Today

What does it mean to formalize mathematics?
Why formalize?
Formalization and mathematics in the age of AI

Formalization

At a low level, formalizing mathematics means writing the axioms of mathematics in a strict formal language, and then using a computer to check proofs line by line
This is nothing new: it started even before the existence of computers
It doesn't look very interesting for most mathematicians

Low-level formalization

Russell and Whitehead's Principia Mathematica.

Proof Assistants

Today, formalization is done with proof assistants
Proof assistants are programming languages that allow one to express mathematical concepts
They allow one to write mathematics in a human-friendly way

Low-level formalization

Forget this

Lean and mathlib

There are various proof assistants (Rocq, Isabelle, Agda, ...); we will focus on Lean
Lean has been developed by Leonardo de Moura at Microsoft Research in 2013
It is an open source software — the current version is Lean 4
Mathlib is Lean's official mathematical library
It covers mathematics at the level of an advanced undergraduate or first-year graduate student
Almost 2.5 million lines of code, contributed by hundreds of people

Parseval's identity: \dfrac{1}{2\pi}\int_{-\pi}^{\pi} |f(x)|^2 \, dx = \sum_{n=-\infty}^{\infty} |\hat f (n)|^2

Condensed spaces: \text{CompHaus}^{\text{op}} \Rightarrow \text{Set}

A Lean example

theorem Heine_Cantor (X Y : Type) [MetricSpace X] [MetricSpace Y] [CompactSpace X]
    (f : X → Y) (hf : Continuous f) : UniformContinuous f := byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous f⊢ UniformContinuous f
  rw [Metric.uniformContinuous_iff]X:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous f⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε
  intros ε ε_posX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε
  let K := { (p₁, p₂) : X × X | ε ≤ dist (f p₁) (f p₂) }X:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε
  have K_closed : IsClosed K := byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous f⊢ UniformContinuous f
    apply isClosed_lehfX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}⊢ Continuous fun b => εhgX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}⊢ Continuous fun b => dist (f b.1) (f b.2)
    ·hfX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}⊢ Continuous fun b => ε continuityAll goals completed! 🐙
    ·hgX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}⊢ Continuous fun b => dist (f b.1) (f b.2) continuityAll goals completed! 🐙
  have K_cpct : IsCompact K := byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous f⊢ UniformContinuous f exact IsClosed.isCompact K_closedAll goals completed! 🐙
  rcases K.eq_empty_or_nonempty with h | hinlX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K = ∅⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < εinrX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonempty⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε
  ·inlX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K = ∅⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε use 1, byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K = ∅⊢ 1 > 0 grindAll goals completed! 🐙
    intros x yrightX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K = ∅x:Xy:X⊢ dist x y < 1 → dist (f x) (f y) < ε
    have : (x, y) ∉ K := byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous f⊢ UniformContinuous f grindAll goals completed! 🐙
    grindAll goals completed! 🐙
  obtain ⟨p, p_in, H⟩ : ∃ p ∈ K, ∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2X:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonempty⊢ ∃ p ∈ K, ∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2inrX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ ∃ δ > 0, ∀ ⦃a b : X⦄, dist a b < δ → dist (f a) (f b) < ε
  ·X:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonempty⊢ ∃ p ∈ K, ∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2 apply K_cpct.exists_forall_le hX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonempty⊢ ContinuousOn (fun x => dist x.1 x.2) K
    continuityAll goals completed! 🐙
  use dist p.1 p.2hX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ dist p.1 p.2 > 0 ∧ ∀ ⦃a b : X⦄, dist a b < dist p.1 p.2 → dist (f a) (f b) < ε
  constructorh.leftX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ dist p.1 p.2 > 0h.rightX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ ∀ ⦃a b : X⦄, dist a b < dist p.1 p.2 → dist (f a) (f b) < ε
  ·h.leftX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ dist p.1 p.2 > 0 simph.leftX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ ¬p.1 = p.2
    intro eqh.leftX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2eq:p.1 = p.2⊢ False
    apply lt_irrefl εh.leftX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2eq:p.1 = p.2⊢ ε < ε
    calc
      ε ≤ 0 := byX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2eq:p.1 = p.2⊢ ε ≤ 0 simpa [eq, K] using p_inAll goals completed! 🐙
      _ < ε := ε_pos
  ·h.rightX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2⊢ ∀ ⦃a b : X⦄, dist a b < dist p.1 p.2 → dist (f a) (f b) < ε intros x x'h.rightX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2x:Xx':X⊢ dist x x' < dist p.1 p.2 → dist (f x) (f x') < ε
    contrapose!h.rightX:TypeY:Typeinst✝²:MetricSpace Xinst✝¹:MetricSpace Yinst✝:CompactSpace Xf:X → Yhf:Continuous fε:ℝε_pos:ε > 0K:Set (X × X) := {(p₁, p₂) | ε ≤ dist (f p₁) (f p₂)}K_closed:IsClosed KK_cpct:IsCompact Kh:K.Nonemptyp:X × Xp_in:p ∈ KH:∀ q ∈ K, dist p.1 p.2 ≤ dist q.1 q.2x:Xx':X⊢ ε ≤ dist (f x) (f x') → dist p.1 p.2 ≤ dist x x'
    aesopAll goals completed! 🐙

Test it live! https://tinyurl.com/4wudt5ex

QR code

Why formalize?

Formalizing looks like explaining mathematics to an alien
Their way of thinking about mathematics is completely different from yours
To make them understand, you have to reorganize and rethink your mathematics
You have to reduce the noise in your mathematics
At the end you have much clearer thinking and a deeper understanding

"The Lean Proof Assistant was really that: an assistant in navigating through the thick jungle that this proof is." — Peter Scholze

Formalization can help understanding

Consider the following easy lemma:

Let (u_n) and (v_n) be sequences of real numbers and \ell \in \mathbb{R}. If \lim u_n = \ell^+ and \lim v_n = -\infty then \lim (u_n + v_n) = -\infty.

It seems like a special case of a more general result about limits of sums of sequences

But which one exactly?

Formalization can help understanding

Consider the following easy lemma:

Let (u_n) and (v_n) be sequences of real numbers and \ell \in \mathbb{R}. If \lim u_n = \ell^+ and \lim v_n = -\infty then \lim (u_n + v_n) = -\infty.

This is done in Lean (and in other proof assistants) using filters

Already done in Bourbaki

Checking correctness

Correctness is checked by the kernel of the proof assistant
The kernel is a relatively small piece of software
A bug in the kernel is very unlikely
In practice the chance that a wrong proof is accepted by the kernel is negligible...
...if the proof is written by humans
But definitions should always be checked very carefully

"I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. I still have some small lingering doubts." — Peter Scholze

AI and formalization

LLMs are getting better and better at formalizing mathematics
A team led by Sidharth Hariharan was able, with the help of AI, to formally verify Viazovska's result on sphere packing in dimension 8
The same model was able to verify the result in dimension 24
Writing a formal proof of one theorem is very different from building a library
Humans are needed to check statements and definitions...
...and also that the AI didn't cheat

Thank You

Thank you for your attention!