lizn-zn/algoveri-lean
AlgoVeri-Lean 77 classical algorithm verification tasks in Lean 4 What is this? This is the Lean 4 subset of the AlgoVeri benchmark — a cross-language benchmark for vericoding (generating formally verified code from specifications). Each task provides a Lean 4 specification that includes: Preconditions — constraints on valid inputs Function signature — with a sorry'd implementation to be filled in Postconditions — formal properties the implementation must… See the full description on the dataset page: https://huggingface.co/datasets/lizn-zn/algoveri-lean.
<div align="center">
AlgoVeri-Lean
77 classical algorithm verification tasks in Lean 4
  
</div>
What is this?
This is the Lean 4 subset of the AlgoVeri benchmark — a cross-language benchmark for vericoding (generating formally verified code from specifications).
Each task provides a Lean 4 specification that includes:
- Preconditions — constraints on valid inputs
- Function signature — with a
sorry'd implementation to be filled in - Postconditions — formal properties the implementation must satisfy
- Theorem stub — a
sorry'd correctness proof to be completed
The goal: implement the algorithm and prove the postconditions hold — all in Lean 4.
Quick numbers
Algorithm categories
Usage
from datasets import load_dataset
ds = load_dataset("lizn-zn/algoveri-lean", split="train")
print(ds[0]["task_id"], ds[0]["lean_code"][:200])Spec structure (example: binary_search)
Every .lean file follows the same pattern:
import Mathlib
-- Precondition
def binary_search_lower_bound_precond (seq : Array Int) (target : Int) : Prop :=
seq.size ≤ 0x7FFFFFFF ∧
(∀ i j : Nat, i < j ∧ j < seq.size → seq.getD i 0 ≤ seq.getD j 0)
-- Implementation stub (fill this in)
def binary_search_lower_bound (seq : Array Int) (target : Int)
(h_precond : ...) : Nat :=
sorry
-- Postcondition
def binary_search_lower_bound_postcond (seq : Array Int) (target : Int)
(result : Nat) (h_precond : ...) : Prop :=
result ≤ seq.size ∧
(∀ i : Nat, i < result → seq.getD i 0 < target) ∧
(∀ i : Nat, result ≤ i ∧ i < seq.size → seq.getD i 0 ≥ target)
-- Prove correctness
theorem binary_search_lower_bound_postcond_satisfied ... := by
sorryCitation
@article{zhao2026algoveri,
title = {AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms},
author = {Haoyu Zhao and Ziran Yang and Jiawei Li and Deyuan He and Zenan Li and Chi Jin and Venugopal V. Veeravalli and Aarti Gupta and Sanjeev Arora},
journal = {arXiv preprint arXiv:2602.09464},
year = {2026}
}License
Apache 2.0 — same as the upstream AlgoVeri repository.