:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Yang, Bowen, Yuan, Yi, Li, Chenyi, Wang, Ziyu, Li, Liangqi, Zhang, Bo, Li, Zhe, Wen, Zaiwen
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2602.01291
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

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

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

CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
by: Long, Wentao, et al.
Published: (2026)

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

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
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)

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

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

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

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

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

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

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

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

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

Limited Math: Aligning Mathematical Semantics with Finite Computation
by: Wen, Lian
Published: (2026)

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)

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
by: Ambridge, Todd Waugh
Published: (2024)

Formal Verification of Parameterized Systems based on Induction
by: Xiu, Jiaqi, et al.
Published: (2025)

A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
by: Watanabe, Kazuki, et al.
Published: (2025)

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

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

On the Cut Elimination of Weak Intuitionistic Tense Logic
by: Wang, Yiheng, et al.
Published: (2024)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
by: Li, Sirui, et al.
Published: (2025)

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

Meta-Mathematics of Computational Complexity Theory
by: Oliveira, Igor C.
Published: (2025)

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

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)

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)

Constructive Ordinal Exponentiation
by: de Jong, Tom, et al.
Published: (2025)

Constructive Quantum Logics
by: Aguilera, Juan P., et al.
Published: (2025)

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

The Complexity of the Constructive Master Modality
by: Santiago-Fernández, Sofía, et al.
Published: (2026)

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
by: Kirst, Dominik, et al.
Published: (2026)

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

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