ZFLean: a framework for set-level mathematics in Lean
Vincent Trélat
cs.LO
Apr 27, 2026 · v1
TL;DR
Presents ZFLean, a Lean 4 library for set-level (ZFC) mathematics on top of Mathlib.
Abstract
We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting hints and small predictable tactics, canonical set-theoretic constructions -- Booleans, naturals, integers, sums/option -- and bridges between ZFC objects and Lean's native types enabling mixed set-level/typed proofs. The layer reduces boilerplate for extensional reasoning while remaining compatible with vanilla Mathlib. We discuss library organization and usage patterns that lower the friction of set-theoretic formalization in a dependently typed assistant. We demonstrate typical use of the framework with a case study exercising our constructions and relational calculus through a proof of an isomorphism theorem on curried functions.
Problem
Doing set-level mathematics in Lean 4 requires extensive boilerplate for extensional reasoning, and there is no ergonomic bridge between Lean's typed world and ZFC-based constructions within a single development.
Approach
ZFLean is a Lean 4 library built on Mathlib's ZFC model that provides a relational calculus for sets with rewriting hints and small predictable tactics, canonical set-theoretic constructions (Booleans, naturals, integers, sums/option), and bridges between ZFC objects and Lean's native types enabling mixed set-level/typed proofs. The library reduces boilerplate for extensional reasoning while remaining compatible with vanilla Mathlib.
Results
The framework is demonstrated through a case study proving an isomorphism theorem on curried functions, exercising the relational calculus and canonical constructions.
