一位开发者在 Lean 4 中实现了红黑树，并完成了所有属性的形式化证明，包括排序性质，但目前仅支持插入操作。排序证明（insert_sorted）的规模较大，作者寻求使用 mathlib 进行优化的建议。这是在定理证明器中形式化验证数据结构的重要进展。
背景
红黑树是计算机科学中常用的自平衡二叉搜索树，而 Lean 是一种用于形式化验证的定理证明器和编程语言。数据结构的形式化验证通过数学证明确保其正确性。
- 来源
- Lobsters
- 发布时间
- 2026年4月1日 17:00
- 评分
- 7.0 / 10