Cover Image

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Santos, Marco Dos, de Saxcé, Hugues, Wang, Haiming, Wang, Ran, Baksys, Mantas, Unsal, Mert, Liu, Junqi, Liu, Zhengying, Li, Jia
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

LeanGeo: Formalizing Competitional Geometry problems in Lean
by: Song, Chendong, et al.
Published: (2025)

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

Formalizing Gröbner Basis Theory in Lean
by: Guo, Junyu, et al.
Published: (2026)

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
by: Wang, Haiming, et al.
Published: (2025)

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)

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

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

Verification of Unbounded Client-Server Systems with Distinguishable Clients
by: Phawade, Ramchandra, et al.
Published: (2026)

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

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

LeanBET: Formally-verified surface area calculations in Lean
by: Ugwuanyi, Ejike D., et al.
Published: (2026)

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

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

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

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

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

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

Unbiasing symmetric monoidal categories in Lean
by: Carlier, Robin
Published: (2026)

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

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 $A_1^{(1)}$ Curve Neighborhoods in Lean 4
by: Huang, Yihe, et al.
Published: (2026)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

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

GFLean: An Autoformalisation Framework for Lean via GF
by: Pathak, Shashank
Published: (2024)

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

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research
by: Gerlach, Lukas
Published: (2026)

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

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

LeanLTL: A unifying framework for linear temporal logics in Lean
by: Vin, Eric, et al.
Published: (2025)

Formalizing zeta and L-functions in Lean
by: Loeffler, David, et al.
Published: (2025)

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

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

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
by: Xu, Rongge, 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)

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