Cover Image

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Ji, Junye
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

Combining Textual and Structural Information for Premise Selection in Lean
by: Petrovčič, Job, et al.
Published: (2025)

Comparative Expressivity for Structured Argumentation Frameworks with Uncertain Rules and Premises
by: Proietti, Carlo, et al.
Published: (2025)

Magnushammer: A Transformer-Based Approach to Premise Selection
by: Mikuła, Maciej, et al.
Published: (2023)

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

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

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

Fixed Point Theorems in Computability Theory
by: Terwijn, Sebastiaan A.
Published: (2024)

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
by: Pusceddu, Daniele, et al.
Published: (2024)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
by: Zhang, Terry Jingchen, et al.
Published: (2025)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

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

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

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

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem
by: Livson, Ori, et al.
Published: (2025)

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

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

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
by: Hulak, David B., et al.
Published: (2026)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Generating Theorems by Generating Proof Structures
by: Wernhard, Christoph
Published: (2026)

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

Intuitionistic Propositional Logic in Lean
by: Trufaş, Dafina
Published: (2024)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Partial Label Learning for Automated Theorem Proving
by: Zombori, Zsolt, et al.
Published: (2025)

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

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

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

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

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

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
by: Kasaura, Kazumi, et al.
Published: (2025)

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

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

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

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

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