Copertina

ZFLean: a framework for set-level mathematics in Lean

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autore principale:	Trélat, Vincent
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Degrees of incomputability, realizability and constructive reverse mathematics
di: Kihara, Takayuki
Pubblicazione: (2020)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
di: Mohamed, Abdalrhman, et al.
Pubblicazione: (2025)

Constructive higher sheaf models with applications to synthetic mathematics
di: Coquand, Thierry, et al.
Pubblicazione: (2026)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
di: Qian, Yicheng, et al.
Pubblicazione: (2025)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
di: Santos, Marco Dos, et al.
Pubblicazione: (2025)

Intuitionistic Propositional Logic in Lean
di: Trufaş, Dafina
Pubblicazione: (2024)

A framework for computing upper bounds in passive learning settings
di: Bordais, Benjamin, et al.
Pubblicazione: (2025)

Lean on Vampire Proofs (Short Paper)
di: Bodingbauer, Jonas, et al.
Pubblicazione: (2026)

Intuitionistic modal logics: a minimal setting
di: Balbiani, Philippe, et al.
Pubblicazione: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
di: Li, Jinzheng, et al.
Pubblicazione: (2026)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
di: Moreira, Walter, et al.
Pubblicazione: (2026)

LeanArchitect: Automating Blueprint Generation for Humans and AI
di: Zhu, Thomas, et al.
Pubblicazione: (2026)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
di: Pertseva, Elizaveta, et al.
Pubblicazione: (2026)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
di: Yang, Bowen, et al.
Pubblicazione: (2026)

Nelson algebras, residuated lattices and rough sets: A survey
di: Järvinen, Jouni, et al.
Pubblicazione: (2024)

Synthetic Differential Geometry in Lean
di: Brasca, Riccardo, et al.
Pubblicazione: (2026)

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research
di: Gerlach, Lukas
Pubblicazione: (2026)

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

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

CSLib: The Lean Computer Science Library
di: Barrett, Clark, et al.
Pubblicazione: (2026)

Unbiasing symmetric monoidal categories in Lean
di: Carlier, Robin
Pubblicazione: (2026)

Formalizing CHSH Rigidity in Lean 4
di: Zhao, Tianrun, et al.
Pubblicazione: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
di: Ji, Junye
Pubblicazione: (2026)

Automated Tactics for Polynomial Reasoning in Lean 4
di: Shen, Hao, et al.
Pubblicazione: (2026)

Formalizing Wu-Ritt Method in Lean 4
di: Xiao, Yuxuan, et al.
Pubblicazione: (2026)

Small Scale Reflection for the Working Lean User
di: Gladshtein, Vladimir, et al.
Pubblicazione: (2024)

The equivariant model structure on cartesian cubical sets
di: Awodey, Steve, et al.
Pubblicazione: (2024)

LeanBET: Formally-verified surface area calculations in Lean
di: Ugwuanyi, Ejike D., et al.
Pubblicazione: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
di: Szeider, Stefan
Pubblicazione: (2026)

Process-Driven Autoformalization in Lean 4
di: Lu, Jianqiao, et al.
Pubblicazione: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
di: Song, Peiyang, et al.
Pubblicazione: (2024)

Bringing memory to Boolean networks: a unifying framework
di: Gadouleau, Maximilien, et al.
Pubblicazione: (2024)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
di: Montesi, Fabrizio, et al.
Pubblicazione: (2026)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
di: Ospanov, Azim, et al.
Pubblicazione: (2025)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
di: Baek, Jineon, et al.
Pubblicazione: (2024)

Premise Selection for a Lean Hammer
di: Zhu, Thomas, et al.
Pubblicazione: (2025)

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

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
di: Henson, Christopher, et al.
Pubblicazione: (2026)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
di: Yin, David, et al.
Pubblicazione: (2025)

On the Possibilities of Hypercomputing Supertasks
di: Müller, Vincent C.
Pubblicazione: (2025)