Sorting algorithms and formal verification in Lean 4.
LeanSort connects executable sorting algorithms with proofs of correctness, execution traces, and operation counts. The core correctness contract is a sorted permutation of the input: no elements lost, added, or duplicated. Implementations and proofs are developed incrementally; their current status is listed below.
The library is designed for studying and extending the mathematics of sorting. It builds on mathlib, CSlib, and Batteries.
Install elan, then run:
git clone https://github.com/Varifold-Lab/LeanSort.git
cd LeanSort
lake buildThe repository pins Lean and its dependencies. lake build checks all proofs
and executable regression examples.
Try this in a Lean file inside the repository:
import LeanSort
open LeanSort.Quick
#eval quickSortResult [3, 1, 2, 1] -- [1, 1, 2, 3]
-- Correctness for every input, including duplicates.
example (xs : List Nat) :
LeanSort.IsSortingResult (· ≤ ·) xs (quickSortResult xs) :=
quickSortResult_spec xsAll listed algorithms have executable implementations available through
import LeanSort. Proved means both sortedness and preservation of every
input occurrence have been established. All 15 algorithms have this correctness
contract proved and integrated into the library.
| Algorithm | Correctness | Execution trace |
|---|---|---|
| Insertion | Proved | Adjacent swaps; shortest sorting trace |
| Bubble | Proved | Adjacent swaps |
| Selection | Proved | Minimum-selection rounds and swaps |
| Merge | Proved | Comparison choices within merges |
| Pancake | Proved | Prefix reversals |
| Quick | Proved | Recursive partition decision trees |
| Heap | Proved | Root extractions |
| Shell | Proved | Gap-labelled passes and swaps |
| Counting | Proved | Histogram updates |
| Radix | Proved | Binary partition decisions |
| Tree | Proved | Insertion comparison paths; checked replay |
| Bucket | Proved | Key-to-bucket placements; checked replay |
| Bitonic | Proved | Comparator schedule; checked replay |
| Introsort | Proved | Partition decisions and insertion/heap leaves; checked replay |
| Powersort | Proved | Original-run boundaries and merges; checked replay |
Correctness, trace verification, cost bounds, and stability have separate coverage. Executable regression checks accompany the proofs but do not replace them.
Bitonic has verified comparator index bounds, exact schedule execution,
and a comparator count of p * d * (d + 1) / 4, where p = 2^d is the padded
length. Its sortedness proof uses the zero-one principle and an exact correspondence
between the mathematical network and the executable array implementation.
Formal cost results include insertion's exact inversion count, selection's
exact n(n−1)/2 comparisons, tree's tight worst-case n(n−1)/2 comparisons,
and the O(n log n) comparison bounds for merge sort, Introsort, and Powersort.
These count specified operations; they do not measure wall-clock time or memory.
Counting, radix, and bucket accept natural-number keys; the other algorithms accept
linearly ordered types.
See the verification guide for all cost bounds, trace-checker guarantees, assumptions, and theorem references.
Introsort's proof covers arbitrary insertion cutoffs and depth budgets, including
heap fallback at zero depth. With its default parameters, the comparison bound
is n * (6 * log₂ n + 20), including partitioning, insertion leaves, and heap leaves.
Powersort also exposes LeanSort.Power.powerSortBy for sorting records by a
total-preorder comparator, with proved correctness and key-based stability.
Its scheduler performs exactly max(r - 1, 0) merges for r natural runs.
Run detection and all merges together use at most n * (log₂ n + 2) key
comparisons, with a formal worst-case O(n log n) bound. The dyadic node-power
specification and logarithmic merge-tree height are also proved.
- Model — shared mathematical definitions.
- Algorithm — executable sorting implementations.
- Verification — correctness, trace semantics, costs, and checks.
Where available, start with Correctness.lean in a verification directory for the sorting
contract or Checks.lean for examples. Dependencies are pinned in
lakefile.toml and lake-manifest.json.
Contributions to implementations, proofs, tests, and documentation are welcome. See CONTRIBUTING.md for the build and pull-request workflow.
LeanSort's original code and documentation are licensed under the Apache License 2.0. Copyright remains with the contributors. See NOTICE for attribution and the retained AKS third-party notices. External dependencies retain their own licenses.