Formalization of Mathematics in ZFC Set Theory using the Lean 4 Proof Assistant
- Domains
- formal mathematics, theorem proving
- Proposed by
- Stephan Merz
and Vincent Trélat
- Institute
-
Inria Research Center at University of Lorraine &
LORIA,
Nancy, France
- Duration
- 5 months, spring or summer 2026
Context
The Lean 4 proof assistant is a modern interactive theorem prover
that has rapidly gained importance in the formalization of mathematics
and in computer science applications. Most existing formalization projects
in Lean (such as Mathlib) are based on dependent type theory.
An alternative line of work investigates the formalization of mathematics
directly in a representation of ZFC set theory.
A clean and usable theory has already been developed, providing a type
ZFSet of ZFC sets. On top of this foundation, standard mathematical
constructions have been formalized, including Boolean algebra (ZFBool),
natural numbers (ZFNat), and integers (ZFInt). Further development
of the library is needed in order to obtain a rich hierarchy of
mathematical objects, ultimately making ZFC formalization in Lean a
viable alternative to type-theoretic approaches.
Objectives
The objective of this internship is to extend the existing ZFC formalization in Lean 4 by:
- Defining the rationals and reals on top of the already available naturals and integers.
- Developing theorems about the structure and basic properties of rational and real numbers.
- Contributing to the broader library of set-theoretic constructions
(functions, finiteness, specific functions such as minimum and maximum, etc.).
Depending on progress and interest, the internship may also explore methodological aspects
(e.g., comparison with type-theoretic formalization, integration with Mathlib).
Expected Work
- Become familiar with Lean 4 as a programming and proof environment.
- Study the existing `ZFSet` library and its constructions.
- Implement the rationals and reals and prove key algebraic and order-theoretic properties.
- Contribute to the development of general theorems on functions and finiteness.
- Produce a technical report. Contributions may be prepared for integration into Mathlib.
Prerequisites
- Solid background in computer science and mathematics at the master level.
- Knowledge of set theory and basic mathematics (algebra, analysis).
- Functional programming experience.
- Prior experience with proof assistants (Lean, Rocq, Isabelle, etc.) is a plus but not mandatory.
Stephan Merz