:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Pertseva, Elizaveta, Robert, Valentin, Barrett, Clark, Parker, James
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2605.15163
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

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

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

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

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

Proof Minimization in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

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

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
by: Przybocki, Benjamin, et al.
Published: (2024)

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

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

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
by: Preiner, Mathias, et al.
Published: (2026)

Generalized Optimization Modulo Theories
by: Tsiskaridze, Nestan, et al.
Published: (2024)

Cubing for Tuning
by: Wu, Haoze, et al.
Published: (2025)

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

Proofs that Modify Proofs, 1/2
by: Towsner, Henry
Published: (2025)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
by: Aniva, Leni, et al.
Published: (2024)

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

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
by: Kolesar, John, et al.
Published: (2025)

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

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
by: Tiurin, Aleksei, et al.
Published: (2024)

Verifying SQL Queries using Theories of Tables and Relations
by: Mohamed, Mudathir, et al.
Published: (2024)

Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
by: Cesco, Arnaldo, et al.
Published: (2021)

Towards Language Model Guided TLA+ Proof Automation
by: Zhou, Yuhao, et al.
Published: (2025)

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

LeanTutor: Towards a Verified AI Mathematical Proof Tutor
by: Patel, Manooshree, et al.
Published: (2025)

The termination of Nielsen transformations applied to word equations with length constraints
by: Przybocki, Benjamin, et al.
Published: (2025)

Lemur: Integrating Large Language Models in Automated Program Verification
by: Wu, Haoze, et al.
Published: (2023)

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

The Proof Analysis Problem
by: Arteche, Noel, et al.
Published: (2025)

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

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

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
by: Yanahama, Banri, et al.
Published: (2026)

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

Proof Complexity of Linear Logics
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2026)

Proof-theoretic Semantics for Second-order Logic
by: Gheorghiu, Alexander V., et al.
Published: (2025)

Proof-theoretic Semantics for the Logic of Bunched Implications
by: Gu, Tao, et al.
Published: (2023)

Proof-theoretic Semantics for First-order Logic
by: Gheorghiu, Alexander V.
Published: (2024)

Cyclic Proofs for iGL via Corecursion
by: Miranda, Borja Sierra
Published: (2023)

An SMT-LIB Theory of Finite Fields
by: Hader, Thomas, et al.
Published: (2024)