ZFLean: a framework for set-level mathematics in Lean

TL;DR

ZFLean is a Lean 4 library that simplifies set-level mathematics within ZFC models, offering tools for canonical constructions, relational calculus, and bridging set theory with Lean's native types.

Contribution

It introduces a relational calculus and canonical set-theoretic constructions in Lean 4, enhancing usability and reducing boilerplate for set-theoretic formalization.

Findings

Developed a relational calculus with rewriting hints and tactics

Built canonical constructions for Booleans, naturals, integers, sums, options

Demonstrated the framework with a proof of an isomorphism theorem on curried functions

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.