Lean 在一个开放平台中结合小型证明检查内核、富表达力的依赖类型理论、交互式证明开发与可扩展自动化，并同时面向形式化数学与验证任务。
2015 年 8 月 7 日 CADE-25 上，Leonardo de Moura 与合作者将 Lean 公开描述为一种新的开源定理证明器：它采用基于依赖类型理论的小型可信内核，并明确以连接交互式与自动定理证明为目标。收录该系统论文的 Springer CADE-25 proceedings 于 2015 年 7 月 30 日出版。Lean 官方历史记录其仓库首次 commit 于 2013 年 7 月、Lean 0.1 正式发布于 2014 年 6 月；由于这些更早记录仅精确到月份，本条采用具有精确日期的 CADE 展示作为 canonical 公开锚点。
该系统后来成为大型形式数学库与学习式定理证明器的长期基础，因此其 2016 年以前的形成是理解 Chronicle 后续大量 Lean 相关 AI4Math 里程碑所必需的历史背景。
重要性说明：Lean 建立了新的依赖类型证明助手平台，并从设计上明确结合交互式定理证明与自动化，为后来的 Lean/mathlib 生态以及现代 AI 辅助形式数学的重要路线奠定技术基础。
Springer 出版收录 Lean 系统论文的 CADE-25 proceedings，记录其架构、目标及在形式数学中的使用。
CADE 官方展示、项目官方历史与保留的开源 Lean 3 仓库使早期系统谱系与实现可直接检查；本记录不根据只有月份精度的历史元数据推断 2014 年 6 月 Lean 0.1 的具体发布日期。
当前没有记录的更正。
