Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.24195 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915961254182912 |
|---|---|
| author | Trélat, Vincent |
| author_facet | Trélat, Vincent |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_24195 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | ZFLean: a framework for set-level mathematics in Lean Trélat, Vincent Logic in Computer Science 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. |
| title | ZFLean: a framework for set-level mathematics in Lean |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2604.24195 |