Buchumschlag

ZFLean: a framework for set-level mathematics in Lean

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
1. Verfasser:	Trélat, Vincent
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Degrees of incomputability, realizability and constructive reverse mathematics
von: Kihara, Takayuki
Veröffentlicht: (2020)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
von: Mohamed, Abdalrhman, et al.
Veröffentlicht: (2025)

Constructive higher sheaf models with applications to synthetic mathematics
von: Coquand, Thierry, et al.
Veröffentlicht: (2026)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
von: Qian, Yicheng, et al.
Veröffentlicht: (2025)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
von: Santos, Marco Dos, et al.
Veröffentlicht: (2025)

Intuitionistic Propositional Logic in Lean
von: Trufaş, Dafina
Veröffentlicht: (2024)

A framework for computing upper bounds in passive learning settings
von: Bordais, Benjamin, et al.
Veröffentlicht: (2025)

Lean on Vampire Proofs (Short Paper)
von: Bodingbauer, Jonas, et al.
Veröffentlicht: (2026)

Intuitionistic modal logics: a minimal setting
von: Balbiani, Philippe, et al.
Veröffentlicht: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
von: Li, Jinzheng, et al.
Veröffentlicht: (2026)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
von: Moreira, Walter, et al.
Veröffentlicht: (2026)

LeanArchitect: Automating Blueprint Generation for Humans and AI
von: Zhu, Thomas, et al.
Veröffentlicht: (2026)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
von: Pertseva, Elizaveta, et al.
Veröffentlicht: (2026)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
von: Yang, Bowen, et al.
Veröffentlicht: (2026)

Nelson algebras, residuated lattices and rough sets: A survey
von: Järvinen, Jouni, et al.
Veröffentlicht: (2024)

Synthetic Differential Geometry in Lean
von: Brasca, Riccardo, et al.
Veröffentlicht: (2026)

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research
von: Gerlach, Lukas
Veröffentlicht: (2026)

Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
von: Mayeux, Arnaud, et al.
Veröffentlicht: (2026)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
von: Rowney, Tate, et al.
Veröffentlicht: (2026)

CSLib: The Lean Computer Science Library
von: Barrett, Clark, et al.
Veröffentlicht: (2026)

Unbiasing symmetric monoidal categories in Lean
von: Carlier, Robin
Veröffentlicht: (2026)

Formalizing CHSH Rigidity in Lean 4
von: Zhao, Tianrun, et al.
Veröffentlicht: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
von: Ji, Junye
Veröffentlicht: (2026)

Automated Tactics for Polynomial Reasoning in Lean 4
von: Shen, Hao, et al.
Veröffentlicht: (2026)

Formalizing Wu-Ritt Method in Lean 4
von: Xiao, Yuxuan, et al.
Veröffentlicht: (2026)

Small Scale Reflection for the Working Lean User
von: Gladshtein, Vladimir, et al.
Veröffentlicht: (2024)

The equivariant model structure on cartesian cubical sets
von: Awodey, Steve, et al.
Veröffentlicht: (2024)

LeanBET: Formally-verified surface area calculations in Lean
von: Ugwuanyi, Ejike D., et al.
Veröffentlicht: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
von: Szeider, Stefan
Veröffentlicht: (2026)

Process-Driven Autoformalization in Lean 4
von: Lu, Jianqiao, et al.
Veröffentlicht: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
von: Song, Peiyang, et al.
Veröffentlicht: (2024)

Bringing memory to Boolean networks: a unifying framework
von: Gadouleau, Maximilien, et al.
Veröffentlicht: (2024)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
von: Montesi, Fabrizio, et al.
Veröffentlicht: (2026)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
von: Ospanov, Azim, et al.
Veröffentlicht: (2025)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
von: Baek, Jineon, et al.
Veröffentlicht: (2024)

Premise Selection for a Lean Hammer
von: Zhu, Thomas, et al.
Veröffentlicht: (2025)

$\text{TT}^{\Box}_{\mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity
von: Cohen, Liron, et al.
Veröffentlicht: (2023)

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
von: Henson, Christopher, et al.
Veröffentlicht: (2026)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
von: Yin, David, et al.
Veröffentlicht: (2025)

On the Possibilities of Hypercomputing Supertasks
von: Müller, Vincent C.
Veröffentlicht: (2025)