:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Rowney, Tate, Ahuja, Riyaz, Avigad, Jeremy, Welleck, Sean
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2602.18657
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
by: Ahuja, Riyaz, et al.
Published: (2026)

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

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

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

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

Implementing Dependent Type Theory Inhabitation and Unification
by: Norman, Chase, et al.
Published: (2026)

Hint-Based SMT Proof Reconstruction
by: Clune, Joshua, et al.
Published: (2026)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
by: Bryant, Randal E., et al.
Published: (2025)

A Proof-Producing Compiler for Blockchain Applications
by: Avigad, Jeremy, et al.
Published: (2025)

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

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

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

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

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

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

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

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

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)

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

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

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
by: Lyon, Tim S., 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)

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

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

ZFLean: a framework for set-level mathematics in Lean
by: Trélat, Vincent
Published: (2026)

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

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
by: Huang, Yihe, et al.
Published: (2026)

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

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

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

Synthetic Differential Geometry in Lean
by: Brasca, Riccardo, et al.
Published: (2026)

A Naive Encoding of Russell's Paradox in Type Theory
by: Qu, Zhuoyuan
Published: (2025)

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

On Small Types in Univalent Foundations
by: de Jong, Tom, et al.
Published: (2021)

Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV
by: Nakamura, Yuki
Published: (2026)

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
by: Mannucci, Mirco A., et al.
Published: (2026)

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

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
by: Shen, Austin, et al.
Published: (2026)

Primitive Recursive Dependent Type Theory
by: Buchholtz, Ulrik, et al.
Published: (2024)