Cover Image

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Tang, Xichen
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Theorem Provers: One Size Fits All?
by: Oates, Harrison, et al.
Published: (2025)

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

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

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

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

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

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

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

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
by: Vin, Eric, et al.
Published: (2025)

A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
by: Barthe, Gilles, et al.
Published: (2025)

Dynamic IFC Theorems for Free!
by: Algehed, Maximilian, et al.
Published: (2020)

Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
by: Casetta, Richard, et al.
Published: (2026)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

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

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

S4 modal sequent calculus as intermediate logic and intermediate language
by: Caspar, Jean, et al.
Published: (2026)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
by: Batz, Kevin, et al.
Published: (2024)

From Semantics to Syntax: A Type Theory for Comprehension Categories
by: Najmaei, Niyousha, et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

Vibe Coding an LLM-powered Theorem Prover
by: Hou, Zhe
Published: (2026)

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
by: Allen, Bradley P.
Published: (2026)

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

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

A Lazy, Concurrent Convertibility Checker
by: Courant, Nathanaëlle, et al.
Published: (2025)

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

A Program Logic for Abstract (Hyper)Properties
by: Baldan, Paolo, et al.
Published: (2026)

A feasible and unitary quantum programming language
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

A Demonic Outcome Logic for Randomized Nondeterminism
by: Zilberstein, Noam, et al.
Published: (2024)

A formalization of System I with type Top in Agda
by: Séttimo, Agustín, et al.
Published: (2026)

A programming language characterizing quantum polynomial time
by: Hainry, Emmanuel, et al.
Published: (2022)

PolyQEnt: A Polynomial Quantified Entailment Solver
by: Chatterjee, Krishnendu, et al.
Published: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

A beginner guide to Iris, Coq and separation logic
by: Dietrich, Elizabeth
Published: (2021)