An Introduction to Formalization of Mathematics

Today

• What does it mean to formalize mathematics?

• Why can formalization be useful to a working mathematician?

• What changes when AI systems can write formal proofs?

• Examples of very recent achievements in research-level formalization

What does it mean to formalize mathematics?

Formalization

At the lowest level, formalization means choosing a very precise language for expressing mathematics, and then asking a computer to check every argument. It means using a computer to reason.

• The idea predates computers.

• Nothing important may be hidden behind “obvious” or “similarly.”

• The result is unambiguous and machine-checkable.

• It is sometimes far from ordinary mathematical style.

Formalization before computers

Principia Mathematica: the proof that 1 + 1 = 2.

Proof assistants

Modern formalization is done with proof assistants: programming languages and interactive tools designed for mathematics.

• They provide notation, automation, and immediate feedback.

• They let us organize results into reusable libraries.

• Humans can write at a much higher level while a small trusted kernel checks the resulting proof term.

• They make large-scale collaboration possible: contributors can trust each other's results without re-reading the proofs.

Lean

• Rocq, Isabelle, Agda, and Lean are among the major proof assistants.

• Leonardo de Moura launched Lean at Microsoft Research in 2013; Lean 4 is the current implementation.

• Lean is open source and is both a functional programming language and a theorem prover.

• Lean has become the proof assistant of choice for many research mathematicians in recent years.

mathlib

• mathlib is Lean's community-maintained mathematical library, developed by hundreds of contributors.

• Its scope ranges from undergraduate mathematics to results used in current research.

• Shared definitions and APIs allow later formalizations to build on earlier work.

• It now contains almost 2.5 million lines of Lean code and continues to grow every day.

• Everything lives in one coherent library, so all results are stated in compatible terms and can be combined freely.

Two examples from mathlib

Parseval's identity

\frac{1}{2\pi}\int_{-\pi}^{\pi}|f(x)|^2\,dx = \sum_{n=-\infty}^{\infty}|\hat f(n)|^2

A condensed set

\mathrm{CompHaus}^{\mathrm{op}} \longrightarrow \mathrm{Set}

The same examples in Lean

Parseval's identity

theorem parseval :
    ∑' n : ℤ, ‖fourierCoeff f n‖ ^ 2 =
      ∫ t, ‖f t‖ ^ 2 ∂haarAddCircle

A condensed set

def CondensedSet :=
  CompHaus.{u}ᵒᵖ ⥤ Type (u + 1)

The Heine–Cantor theorem

Theorem. Let X and Y be metric spaces, with X compact. Every continuous f : X \to Y is uniformly continuous.

Proof. Fix \varepsilon > 0 and set

K_\varepsilon = \{(x,y) \in X \times X \mid \varepsilon \le d_Y(f(x),f(y))\}.

K_\varepsilon is closed in compact X \times X, hence compact. Choose (p,q) \in K_\varepsilon minimizing d_X(p,q), and set \delta=d_X(p,q).

• \delta>0: otherwise p=q, giving \varepsilon \le d_Y(f(p),f(q))=0.

• If d_X(x,y)<\delta and d_Y(f(x),f(y))\ge\varepsilon, then (x,y)\in K_\varepsilon, so minimality gives \delta\le d_X(x,y), a contradiction.

Therefore f is uniformly continuous. \square

In the formalization we will rely on mathlib for all the notions and theorems not fully explained here.

Of course mathlib also contains the theorem itself.

Why can formalization be useful to a working mathematician?

Why formalize?

• Formalization forces us to think clearly and precisely.

• It often reveals the need for new abstractions.

• It requires us to organize the mathematics more effectively and strip away unnecessary noise.

• In the end, the process leads to a deeper understanding of the mathematics.

• It turns mathematics into data that software — and AI systems — can search and build on.

• It catches errors and hidden assumptions that can survive even careful human refereeing.

An example of generalization: semirings

mathlib tries to state results under the weakest natural assumptions. For example, in every commutative semiring,

(a+b)^2 = a^2 + 2ab + b^2

• The most familiar example is \mathbb{N}.

• Less obviously, the ideals of a commutative ring themselves form a semiring.

• More importantly, this level of abstraction gives us a general theory of free modules and rank over semirings, under remarkably weak assumptions.

Another generalization

Let (u_n) and (v_n) be real sequences and \ell \in \mathbb{R}. Suppose u_n \to \ell from above and v_n \to -\infty. Then

u_n + v_n \to -\infty

This looks like a special case of a theorem about sums of sequences. Which theorem, exactly?

The useful abstraction is convergence along suitable filters. This language was introduced by Bourbaki to treat different forms of convergence uniformly.

• Filters separate the algebra of addition from the many possible notions of convergence.

• The same theorem can then cover ordinary convergence, one-sided limits, and divergence to infinity.

• Formalization makes the choice of this abstraction unavoidable in practice.

Filters and convergence

A filter on a set X is a family F of subsets of X — the “large” subsets — such that:

• X \in F;

• if A \in F and A \subseteq B, then B \in F;

• if A \in F and B \in F, then A \cap B \in F.

Examples. The neighborhoods of a point x; the subsets of \mathbb{R} containing some [N, +\infty) — a “neighborhood of +\infty”, written \operatorname{atTop}; the sets containing some (\ell, \ell+\varepsilon), for convergence to \ell from above.

Convergence. Given f : X \to Y and filters F on X and G on Y, we say that f tends to G along F if

f^{-1}(S) \in F \quad \text{for every } S \in G.

Ordinary limits, one-sided limits, and divergence to \pm\infty become one notion: u_n \to \ell says u tends to \mathcal{N}_\ell along \operatorname{atTop}, and v_n \to -\infty says v tends to \operatorname{atBot} along \operatorname{atTop}.

A proof assistant can assist

The Liquid Tensor Experiment formally verified a recent theorem from Peter Scholze's work with Dustin Clausen on condensed mathematics.

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

Asked what else he learned from the formalization: “What actually makes the proof work! When I wrote the blog post half a year ago, I did not understand why the argument worked, and why we had to move from the reals to a certain ring of arithmetic Laurent series.” — Peter Scholze

What changes when AI systems can write formal proofs?

What exactly is checked?

• Lean's kernel checks the final proof term, independently of the tactics or AI system that produced it.

• The kernel is deliberately small, making the trusted core easier to audit and reimplement.

• Compiled proofs can be re-verified by independent external checkers, written in different languages by different authors.

• A successful check proves the formal statement from the declared assumptions.

• A verified proof is only as meaningful as its statement: a wrongly stated theorem checks just as well.

Human review is still needed for statements, definitions, assumptions, and library design.

AI and formalization

• Language models are increasingly capable of translating arguments and filling proof gaps in Lean.

• Kernel checking makes the output verifiable regardless of how a proof was produced.

• Formalization solves the trust problem of AI mathematics: a hallucinated proof simply does not compile.

• Formal verification does not remove the need to review statements, definitions, or library architecture.

• The mathematician's role shifts in certain cases toward stating the right definitions and theorems, and judging what is worth proving.

Three levels of trust

• Lean accepts the file. The weakest check: nothing is red in the editor. A sorry, a warning switched off, or a plausible-looking tactic that admits the goal all pass. Enough for everyday use.

• #print axioms is clean. Enough for most projects.

• Comparator. The gold standard: we fix the statement in advance, in a form simple enough to check by eye, and the proof can be replayed by other kernels.

The first two levels assume the author is not adversarial. Once an LLM is in the loop, only the third one is a check.

Checking statements and definitions is still the work of humans.

Examples of very recent achievements in research-level formalization

Sphere packing

• A project initiated by Sidharth Hariharan and Maryna Viazovska formally verified the sphere-packing results in dimensions 8 and 24: genuinely research-level mathematics, whose original proofs date from 2016 and won Viazovska a Fields Medal.

• Math, Inc.'s Gauss system provided substantial assistance in the final stages, on top of a human-built library, a mathematical blueprint, and close collaboration between mathematicians, formalizers, and AI.

• Along the way the project contributed reusable theory — modular forms, Poisson summation, Fourier analysis — back to mathlib.

• It was the human work — above all writing the blueprint — that made such a fast formalization possible.

A recent project: Kummer's criterion

• An AI-assisted project, joint with Chris Birkbeck, that formalizes Kummer's characterization of the regular primes.

• About 50K lines of Lean, done with the help of Claude Code and Codex in roughly a month.

• It builds on the earlier flt-regular formalization of Fermat's Last Theorem for regular primes.

• An odd prime p is regular if it does not divide the class number of the cyclotomic field, p \nmid h(\mathbb{Q}(\zeta_p)).

• Kummer's criterion. p is regular if and only if p divides none of the numerators of the Bernoulli numbers B_2, B_4, \dots, B_{p-3}.

Which proof to formalize?

• The classical proof of Kummer's criterion goes through class field theory (CFT).

• At first the AI agents were convinced they could sidestep CFT entirely.

• In the end we found a different proof, assembling several pieces already scattered across the literature.

• Guided by us, the models were much more efficient than when left to work alone.

Kummer's criterion and Fermat

Kummer proved Fermat's Last Theorem for every regular prime exponent.

• The criterion makes regularity checkable: the only irregular primes below 100 are 37, 59, and 67.

• We also have a separate proof of FLT for the smallest irregular exponent, n = 37.

• Combined with the flt-regular project, this yields FLT for every exponent under 100 except 59 and 67.

• The project also formalizes Carlitz's proof that there are infinitely many irregular primes.

Three counterexamples

Formalization is not only about proving theorems. Increasingly, AI systems propose counterexamples, and Lean is used to certify that they really work.

In the last two months alone, three notable counterexamples were found by AI — all now verified in Lean:

• the Erdős unit-distance conjecture,

• a 60-year-old question of Grothendieck on finite group schemes,

• the Jacobian conjecture, open for almost a century.

In each case a human still had to state the problem and check the formal proof.

Counterexample I: the Erdős unit-distance conjecture

Conjecture (Erdős, 1946). The number of pairs at distance exactly 1 among n points in the plane is at most n^{1+o(1)}.

• On May 20th, 2026 ChatGPT produced a point configuration with far more unit distances than this bound allows, using the Golod–Shafarevich theorem from number theory (1960s) to drive the construction.

• Boris Alexeev (OpenAI) then formalized the entire argument in Lean with the Sol model — about 1.2 million lines in roughly three weeks, assuming nothing beyond the axioms: even global class field theory was built from scratch.

Counterexample II: finite group schemes

Question (Grothendieck). Is every finite locally free group scheme of order n killed by n, i.e. do all its points x satisfy x^n = 1?

• Deligne proved it for commutative group schemes, Grothendieck for reduced bases, and Schoof pushed it further.

• At the Formalizing Fermat workshop, Akhil Mathew posed it to Fable, who solved it.

The group-scheme counterexample

R = \mathbb{Z}[a,b] \,/\, (a^3,\; b^3,\; a^2b + 2), \qquad \operatorname{char} R = 4

A = R[U,V] \,/\, (\,U^2 - abU + b^2V,\;\; V^2 - a^2V\,)

\operatorname{rank}_R A = 4

\lambda = (1 + aU)(1 + bV), \qquad \lambda^4 = 1, \qquad \Delta\lambda = \lambda \otimes \lambda

\Delta U = U \otimes 1 + \lambda \otimes U, \qquad \Delta V = V \otimes \lambda + 1 \otimes V

\varepsilon(U) = \varepsilon(V) = 0

[n]\,U = \bigl(1 + \lambda + \cdots + \lambda^{\,n-1}\bigr)\,U

[4]\,U = 2bUV \neq 0, \qquad [8] = [0]

Immediately formalized in Lean.

Counterexample III: the Jacobian conjecture

Conjecture (Keller, 1939). Let F : \mathbb{C}^n \to \mathbb{C}^n be a polynomial map whose Jacobian determinant \det\!\big(\partial F_i/\partial x_j\big) is a nonzero constant. Then F is bijective, with a polynomial inverse.

• Open for almost a century, and the graveyard of many false proofs.

• On July 19th Levent Alpöge used Fable to produce a counterexample, immediately formalized in Lean.

The Jacobian counterexample

F(X,Y,Z) = \begin{pmatrix} (1+2XY)^3\,Z + 4Y^2(1+2XY)(2+3XY) \\ Y + 3X(1+2XY)^2\,Z + 12XY^2(2+3XY) \\ -X + 3X^2Y + X^3Z \end{pmatrix}

\det \operatorname{Jac} F = 1

F\bigl(1,\, -\tfrac{3}{4},\, \tfrac{13}{4}\bigr) = F\bigl(-1,\, \tfrac{3}{4},\, \tfrac{13}{4}\bigr)

Final thoughts

• Discussions are under way to really understand where these counterexamples come from.

• If AI had found these counterexamples immediately, would we have missed some good mathematics developed along the way?

• The future looks more and more like human–AI collaboration, with formal verification in the loop.

Thank you

Thank you for your attention!