ZFLean: a framework for set-level mathematics in Lean

Vincent Tr\'elat

arxiv: 2604.24195 · v1 · submitted 2026-04-27 · 💻 cs.LO

ZFLean: a framework for set-level mathematics in Lean

Vincent Tr\'elat This is my paper

Pith reviewed 2026-05-08 01:22 UTC · model grok-4.3

classification 💻 cs.LO

keywords ZFLeanLean 4ZFCset theoryformal verificationMathlibrelational calculusdependent types

0 comments

The pith

ZFLean adds relational calculus and type bridges to enable set-level mathematics in Lean with Mathlib-style ergonomics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

ZFLean is a Lean 4 library built on an existing ZFC model that lets users carry out core mathematics at the set level while keeping the convenience normally associated with typed developments. It supplies a relational calculus equipped with rewriting hints and compact tactics, standard set constructions such as Booleans and natural numbers, and explicit bridges that connect ZFC objects to Lean's native types. These additions cut down the repetitive work of extensional reasoning without breaking compatibility with ordinary Mathlib code. A case study on an isomorphism theorem for curried functions shows how the pieces work together in mixed set-level and typed proofs.

Core claim

ZFLean provides a framework in Lean 4 for formalizing mathematics inside a model of ZFC that maintains the ergonomics of typed developments in Mathlib. By layering a relational calculus with hints and tactics over Mathlib's ZFC, along with canonical set constructions and bridges to native Lean types, the library enables mixed proofs that combine set-level extensionality with type-level convenience. The design ensures compatibility with vanilla Mathlib while lowering the boilerplate typically required for set-theoretic formalizations in a dependently typed prover.

What carries the argument

The relational calculus for sets together with rewriting hints, small predictable tactics, canonical constructions, and bridges between ZFC objects and Lean's native types.

If this is right

Set-theoretic proofs can be written with substantially less boilerplate for extensionality arguments.
Mixed proofs that combine ZFC sets with Lean's native types become practical inside the same development.
Standard constructions such as integers, sums, and options are immediately available at the set level.
Library organization patterns emerge that support typical set-theoretic formalizations while staying compatible with existing Mathlib code.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The approach could make it simpler to formalize theorems from analysis or algebra that are most naturally stated in set language.
If the bridges prove efficient, some existing set-based formal libraries might be adapted into Lean environments with less rewriting.
Wider use of such a layer might encourage more mathematicians to explore set-theoretic methods within Lean without leaving the typed ecosystem.

Load-bearing premise

The added relational calculus, tactics, and bridges between ZFC objects and native Lean types can be implemented without introducing inconsistencies or excessive overhead in the underlying Mathlib ZFC model.

What would settle it

A concrete demonstration that any theorem proved inside ZFLean becomes inconsistent when checked against the plain Mathlib ZFC model, or that typical proofs require substantially more computational resources than equivalent direct Mathlib developments.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

ZFLean layers practical ergonomics on Mathlib's ZFC model without breaking compatibility, and the case study shows it working in a real proof.

read the letter

This paper describes ZFLean, a Lean 4 library that sits on top of Mathlib's existing ZFC model and adds a relational calculus, some small tactics, canonical constructions for basics like booleans and naturals, and bridges to native Lean types. The goal is to cut down on the repetitive extensional reasoning that usually comes with set-level work inside a dependently typed prover. The architecture is explicitly additive, which keeps it compatible with ordinary Mathlib developments. That is the main new piece: the specific combination of relational primitives and mixed-mode bridges rather than another full ZFC formalization from scratch. The case study on an isomorphism theorem for curried functions exercises the new tools in an ordinary proof, which helps show how the layer is meant to be used. Library organization and usage patterns are also laid out, which is useful for anyone who might want to try it. The central claim that boilerplate drops while staying sound looks plausible from the design and the example. No load-bearing circularity or hidden re-axiomatization appears. The main soft spot is that the reduction in boilerplate is described rather than measured with concrete counts or user timing, though for a library paper the working case study and additive structure count as reasonable evidence. Overhead and universe issues are addressed at the level of the architecture but not with exhaustive benchmarks. This is aimed at Lean users who already do formal mathematics and want set-theoretic reasoning to feel less clunky. A reader working on core math formalizations in Mathlib will find the design choices and the concrete example worth looking at. It deserves a serious referee because it is a grounded, reproducible tool contribution that addresses a real friction point in the ecosystem.

Referee Report

1 major / 2 minor

Summary. The manuscript presents ZFLean, a Lean 4 library built atop Mathlib's existing ZFC model. It contributes a relational calculus for sets equipped with rewriting hints and small predictable tactics, canonical constructions for Booleans, naturals, integers, sums, and options, and bridges allowing mixed ZFC-object and native-Lean-type reasoning. The layer is claimed to reduce boilerplate for extensional reasoning while preserving full compatibility with vanilla Mathlib. Library organization, usage patterns, and a case study (an isomorphism theorem for curried functions) are discussed to illustrate typical set-theoretic formalization workflows.

Significance. If the library delivers the promised reduction in extensional boilerplate without introducing inconsistencies or excessive overhead, the contribution would be significant for the Lean community. The explicitly additive architecture (no re-axiomatization of Mathlib's ZFC model) and the concrete case study that exercises the new primitives inside ordinary Lean proofs are clear strengths. Such tooling could lower the friction of set-level formalization while remaining interoperable with the broader Mathlib ecosystem.

major comments (1)

[Case study] The central claim that the relational calculus and bridges 'measurably reduce boilerplate' is load-bearing yet supported only by a single qualitative case study. A side-by-side comparison of proof size or tactic invocations with and without ZFLean (perhaps in § on the isomorphism theorem) would be required to substantiate the claim.

minor comments (2)

The abstract refers to 'small predictable tactics' and 'rewriting hints'; the main text should explicitly list these tactics and their rewrite rules so readers can assess their scope and predictability.
Notation for the relational calculus (e.g., how membership, equality, and function application are written) should be introduced once in a dedicated subsection and then used consistently.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and positive recommendation. We address the single major comment below.

read point-by-point responses

Referee: [Case study] The central claim that the relational calculus and bridges 'measurably reduce boilerplate' is load-bearing yet supported only by a single qualitative case study. A side-by-side comparison of proof size or tactic invocations with and without ZFLean (perhaps in § on the isomorphism theorem) would be required to substantiate the claim.

Authors: We agree that the manuscript supports the reduction in boilerplate through a single qualitative case study rather than quantitative metrics. The case study demonstrates typical usage of the relational calculus, canonical constructions, and type bridges within an ordinary Lean proof of an isomorphism theorem for curried functions. While a side-by-side comparison of proof sizes or tactic counts could offer additional substantiation, we maintain that it is not required to establish the framework's value: the contribution centers on the additive design, library organization, and interoperability with Mathlib, with the case study serving to illustrate workflow patterns. We have partially revised the manuscript by expanding the case study section with explicit annotations that identify the specific extensional boilerplate steps eliminated at each stage of the proof. This clarifies the practical benefit without duplicating the full theorem in a baseline style, which would lengthen the paper disproportionately to the added insight. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The manuscript describes the design and implementation of a new Lean 4 library (ZFLean) that layers relational calculus, tactics, canonical constructions, and ZFC-to-native bridges atop Mathlib's existing ZFC model. No equations, predictions, fitted parameters, or uniqueness theorems are presented; the central claims concern library organization, boilerplate reduction, and compatibility, which are substantiated by explicit code patterns and a concrete case study rather than by reduction to prior self-referential definitions or self-citations. The work is additive and self-contained against external benchmarks (Lean/Mathlib), satisfying the criteria for a non-circular library contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The library rests on Mathlib's existing ZFC model and standard Lean type theory; no new free parameters or invented entities are introduced.

axioms (2)

standard math ZFC axioms as already modeled in Mathlib
The framework explicitly builds on Mathlib's ZFC model for its set-theoretic foundation.
domain assumption Compatibility with vanilla Mathlib developments
The paper states the layer remains compatible with existing Mathlib code.

pith-pipeline@v0.9.0 · 5425 in / 1244 out tokens · 38436 ms · 2026-05-08T01:22:25.416220+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

5 extracted references · 5 canonical work pages

[1]

doi:10.1016/S0049-237X(08)71989-X. V. Trélat XX:17 2 Peter Aczel and Michael Rathjen. Notes on constructive set theory. Technical report, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences),

work page doi:10.1016/s0049-237x(08)71989-x
[2]

4 Georg Cantor

URL: https://doi.org/10.6092/issn.1972-5787/1695,doi:10.6092/ISSN.1972-5787/1695. 4 Georg Cantor. Grundlagen einer allgemeinen Mannigfaltigkeitslehre.Mathematische Annalen, 46:481–512,

work page doi:10.6092/issn.1972-5787/1695 1972
[3]

AN ELEMENTARY THEORY OF THE CATEGORY OF SETS

URL:https://www.pnas.org/doi/ pdf/10.1073/pnas.52.6.1506,doi:10.1073/pnas.52.6.1506. 6 Mathlib Community. Mathlib documentation: ZFC model of sets ( PSet, ZFSet),

work page doi:10.1073/pnas.52.6.1506
[4]

7 Alexandre Miquel

URL: https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/ ZFC/Basic.html. 7 Alexandre Miquel. lamda-z: Zermelo’s set theory as a PTS with 4 sorts. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors,Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, ...

work page doi:10.1007/11617990 2004
[5]

URL: https://leanprover-community.github.io/papers/mathlib-paper.pdf, doi: 10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824

[1] [1]

doi:10.1016/S0049-237X(08)71989-X. V. Trélat XX:17 2 Peter Aczel and Michael Rathjen. Notes on constructive set theory. Technical report, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences),

work page doi:10.1016/s0049-237x(08)71989-x

[2] [2]

4 Georg Cantor

URL: https://doi.org/10.6092/issn.1972-5787/1695,doi:10.6092/ISSN.1972-5787/1695. 4 Georg Cantor. Grundlagen einer allgemeinen Mannigfaltigkeitslehre.Mathematische Annalen, 46:481–512,

work page doi:10.6092/issn.1972-5787/1695 1972

[3] [3]

AN ELEMENTARY THEORY OF THE CATEGORY OF SETS

URL:https://www.pnas.org/doi/ pdf/10.1073/pnas.52.6.1506,doi:10.1073/pnas.52.6.1506. 6 Mathlib Community. Mathlib documentation: ZFC model of sets ( PSet, ZFSet),

work page doi:10.1073/pnas.52.6.1506

[4] [4]

7 Alexandre Miquel

URL: https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/ ZFC/Basic.html. 7 Alexandre Miquel. lamda-z: Zermelo’s set theory as a PTS with 4 sorts. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors,Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, ...

work page doi:10.1007/11617990 2004

[5] [5]

URL: https://leanprover-community.github.io/papers/mathlib-paper.pdf, doi: 10.1145/3372885.3373824

work page doi:10.1145/3372885.3373824