Buchumschlag

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Qian, Yicheng, Clune, Joshua, Barrett, Clark, Avigad, Jeremy
Format:	Preprint
Veröffentlicht:	2025
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

Canonical for Automated Theorem Proving in Lean
von: Norman, Chase, et al.
Veröffentlicht: (2025)

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

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

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
von: Pusceddu, Daniele, et al.
Veröffentlicht: (2024)

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

Hint-Based SMT Proof Reconstruction
von: Clune, Joshua, et al.
Veröffentlicht: (2026)

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

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

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

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
von: Tang, Xichen
Veröffentlicht: (2025)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
von: Aniva, Leni, et al.
Veröffentlicht: (2026)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
von: Shen, Ziju, et al.
Veröffentlicht: (2025)

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

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

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
von: Ahuja, Riyaz, et al.
Veröffentlicht: (2026)

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

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

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

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
von: Jin, Xiangyu, et al.
Veröffentlicht: (2024)

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

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

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

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

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

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

Proof Recommendation System for the HOL4 Theorem Prover
von: Dekhil, Nour, et al.
Veröffentlicht: (2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving
von: Kumarappan, Adarsh, et al.
Veröffentlicht: (2024)

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

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

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
von: Klaus, Natalia, et al.
Veröffentlicht: (2026)

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

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

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

Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
von: Sonoda, Sho, et al.
Veröffentlicht: (2026)

Theorem Provers: One Size Fits All?
von: Oates, Harrison, et al.
Veröffentlicht: (2025)

Vibe Coding an LLM-powered Theorem Prover
von: Hou, Zhe
Veröffentlicht: (2026)

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

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

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

ZFLean: a framework for set-level mathematics in Lean
von: Trélat, Vincent
Veröffentlicht: (2026)