A developer has implemented a red-black tree in Lean 4 with formal proofs for all properties, including sorting, though only insertion is currently supported. The proof for sorted insertion (insert_sorted) is notably large, and the author seeks suggestions for optimization using mathlib. This represents a significant step in formally verified data structures within theorem provers.
Background
Red-black trees are self-balancing binary search trees commonly used in computer science, while Lean is a theorem prover and programming language for formal verification. Formal verification of data structures ensures correctness by mathematical proof.
- Source
- Lobsters
- Published
- Apr 1, 2026 at 05:00 PM
- Score
- 7.0 / 10