Lean语言如何连接数学与编程
本文基于Leo de Moura在2024年7月国际计算机辅助验证会议（CAV）上的主题演讲改编。
Lean项目概述
2013年，Lean项目启动，旨在弥合自动化与交互式定理证明器之间的差距。自成立以来，Lean在数学界的采用率空前，超越了以往形式化数学领域的努力。最新版本Lean 4使用Lean自身实现，同时也是一个功能齐全、可扩展的编程语言，具有强大的IDE支持、包管理和活跃的生态系统。
2023年，Sebastian Ullrich与作者共同创立了Lean聚焦研究组织（FRO），这是一个致力于推进Lean发展并支持其社区的非营利机构。Lean项目秉承促进去中心化创新的理念，赋能多元化的研究人员、开发者和爱好者社区，共同推动数学实践和软件开发的边界。
Lean简介
Lean是一种开源、可扩展的函数式编程语言和交互式定理证明器，使编写正确且可维护的代码变得简单。Lean编程主要涉及定义类型和函数，让用户能够专注于问题领域及其数据，而非编码细节。Lean有四个主要应用场景：形式化数学、软硬件验证、AI辅助数学与代码合成，以及数学与计算机科学教育。
形式化数学
Lean允许数学家使用对他们来说感觉自然的语法处理高级数学结构。数学界认可其实用性：例如，菲尔兹奖得主Peter Scholze和Terence Tao使用Lean验证他们的新结果；《量子杂志》将Lean誉为数学领域最大突破之一，并且其已被众多流行科学和学术出版物报道。
截至2024年7月，Lean数学库已收到超过300位数学家的贡献，包含158万行代码，在使用中的形式化数学系统中居于领先地位。这一显著增长是在Lean简洁且年轻的情况下实现的：它比同类库至少年轻十年。
软硬件验证
Lean将形式化验证、用户交互和数学严谨性相结合，使其对软硬件验证极具价值。Lean是一个既可编程证明又可验证程序的系统。额外优势是Lean能生成高效代码，其最初为数学家设计的可扩展特性，对于编写清晰可维护代码时创建抽象也非常方便。其益处延伸至任何需要极高精度和安全性的系统，包括航空航天、密码学、Web服务、自动驾驶汽车、生物医学系统和医疗设备等行业。
AI辅助数学与代码合成
Lean受到开发数学和代码合成AI的团体欢迎。关键原因之一是Lean的形式化证明可由机器检查，并能通过外部证明检查器独立审计。此外，Lean的可扩展性允许用户深入系统内部，包括表示证明和代码的数据结构。此功能也用于从Lean证明自动生成动画。
AI研究人员正在利用大语言模型创建Lean形式化证明，并自动将散文翻译成形式化数学。某机构发布了基于Lean的强化学习环境lean-gym。某机构在其数学超级智能平台开发中使用了Lean，该AI模型旨在保证准确性并避免幻觉。某机构创建的AI模型已解决10个国际数学奥林匹克竞赛问题，某机构则在Lean中形式化了与AI安全相关的理论结果。此外，LeanDojo是一个使用大语言模型自动化Lean中证明构建的开源项目。
Lean将机器可检查证明、系统内省和可扩展性独特结合，使其成为推进数学和代码合成AI研究的理想工具。
数学与计算机科学教育
数百万人在学生时代学习数学并在整个职业生涯中使用它。自成立以来，Lean项目一直支持学生的数学推理需求，并使更多样化的人群能够为数学和计算机科学领域做出贡献。有多种教育资源可用于学习Lean，包括互动电脑游戏、计算机科学和数学教科书、大学课程和按需教程。Lean FRO致力于扩展Lean的教育内容，并设想一个孩子们使用Lean作为学习数学的游乐场的未来，按照自己的节奏进步并获得即时反馈，类似于许多人学习编码的方式。
Lean快速导览
Lean结合了编程和形式化验证。让我们通过一个小例子快速了解如何在Lean中编写代码并证明关于该代码的属性。
在Lean中编写代码
首先，定义一个连接两个列表的简单函数：
def append (xs ys : List a) : List a :=match xs with| [] => ys| x :: xs => x :: append xs ys
此函数使用模式匹配定义。对于基本情况，将空列表[]附加到ys得到ys。符号x :: xs表示头为x尾为xs的列表。对于递归情况，将x :: xs附加到ys得到x :: append xs ys。此外，append函数是多态的，意味着它适用于任何类型a的列表。
可扩展语法
上面使用的符号x :: xs并非内置到Lean中，而是使用infixr命令定义：
infixr:67 " :: " => List.cons
infixr命令定义了一个新的中缀运算符x :: xs，表示List.cons x xs。此命令实际上是使用Lean的卫生宏系统实现的宏。Lean的可扩展语法允许用户定义自己的领域特定语言。
证明代码属性
接下来，我们将证明关于append函数的一个属性：连接后列表的长度是它们长度之和。
theorem append_length (xs ys : List a): (append xs ys).length = xs.length + ys.length := byinduction xs with| nil => simp [append]| cons x xs ih => simp [append, ih]; omega
这里，theorem引入了一个名为append_length的新定理。语句(append xs ys).length = xs.length + ys.length是我们要证明的。by ...块包含证明。在此证明中：
induction xs with启动对xs的归纳证明；nil情况使用Lean简化器simp证明基本情况，参数append指示简化器展开append的定义；cons x xs ih情况证明归纳步骤，其中ih是归纳假设，也使用simp和完成算术推理的omega。
在此证明中，induction、simp和omega是策略。策略是将证明的一种状态转换为另一种状态的关键，在Lean的交互式定理证明中至关重要。
Lean在某机构的实际应用
在某机构，Lean被用于多个开源项目，以应对复杂的验证和建模挑战。这些项目不仅突出了Lean在不同领域的实际应用，也强调了某机构对开源开发和协作的承诺。我们涵盖四个关键项目：Cedar、LNSym和SampCert（其Lean源代码已在GitHub上可用），以及AILean（正在探索大语言模型与形式化数学的关系，其代码尚未开源）。
Cedar：开源策略语言和评估引擎
Cedar是一种开源策略语言和评估引擎。Cedar使开发人员能够将细粒度权限表达为易于理解的策略，并在其应用程序中强制执行，从而将访问控制与应用程序逻辑解耦。Cedar支持常见的授权模型。它是首个从头开始构建，使用自动化推理进行形式化验证，并利用差分随机测试进行严格测试的策略语言。
Cedar项目使用Lean为Cedar运行时的每个核心组件创建可执行的形式化模型。该模型作为高度可读的规范，允许团队使用Lean证明关键的正确性属性。
选择Lean对Cedar建模是因为其快速的运行时、广泛的库、IDE支持和小型可信计算基。快速的运行时支持Cedar模型的高效差分测试。这些库提供了由开源社区构建的可重用验证数据结构和策略。Lean的小型可信计算基使Cedar能够自信地利用这些贡献，因为Lean检查其正确性，仅需要信任Lean的最小证明检查内核。
LNSym：密码学验证的符号模拟
LNSym是Armv8原生代码程序的符号模拟器。目前正在开发中，重点在于实现对密码机器代码程序的自动化推理。许多密码例程用汇编语言编写，以优化底层处理器的性能和安全性。LNSym旨在降低验证密码例程的成本，最终使密码学开发人员能够对其原生代码程序进行形式化推理。
LNSym使用Lean作为建模Arm指令语义和密码协议的形式化规范语言，并作为推理这些工件的定理证明器。由于Lean程序是可执行的，规范通过全面的一致性测试实现了高度信任。Lean协调证明，使得繁重且通常繁琐的工作通过决策程序自动完成。当证明自动化失败时，用户可以将Lean用作交互式定理证明器。这种交互式与自动化定理证明的结合确保了验证任务的进展不受证明自动化限制的阻碍。
SampCert：形式化验证的差分隐私原语
SampCert是一个形式化验证的差分隐私原语开源库，被某机构清洁房间差分隐私服务用于其快速且可靠的采样算法。使用Lean，SampCert提供了离散高斯采样器的唯一验证实现。
尽管SampCert专注于软件，但其验证严重依赖于Mathlib（Lean数学库）。解决数据隐私实际问题的代码验证依赖于从傅里叶分析到数论和拓扑的数学概念的形式化。
AILean：AI用于数学与数学用于AI
AILean正在探索大语言模型与形式化数学的关系。这种探索是双向的：AI用于数学和数学用于AI。在AILean中，大语言模型用于增强形式化数学中的证明自动化和用户体验。大语言模型可以分析定理陈述和现有证明步骤，建议相关的引理、定义或策略，以指导用户完成证明。它们还可以识别常见错误或不一致之处，提出修正或替代方法，从而改进证明开发过程。
关键要点
Lean是一个复杂系统，但其正确性仅依赖于一个小的可信内核。此外，所有证明和定义都可以导出并独立审计和检查。这对于数学和软件验证社区来说是一个关键特性，因为它消除了信任瓶颈。无论您是谁；如果Lean检查了您的证明，全世界都可以在此基础上构建。这使得从未谋面的大型数学家群体能够协作并共同工作。此外，它允许用户扩展Lean，而无需担心引入可能损害系统逻辑一致性的可靠性错误。
Lean的可扩展性支持定制，这在其资源有限的前十年尤为重要。Lean的可扩展性允许社区扩展系统，而无需与其开发人员同步。自托管，或在Lean中实现Lean，也确保了用户无需学习不同的编程语言即可访问系统的所有部分。这使得扩展Lean变得简单方便。
某机构引入的FRO模型在支持Lean并帮助其过渡到自给自足的基础方面发挥了重要作用。Lean项目已显著成长，如果没有某机构确保慈善支持的努力，推动其前进将会很困难。正如某机构和某机构基金会对开源项目的成功和可持续性至关重要一样，某机构的支持对Lean的持续进展也至关重要。
要了解更多关于Lean的信息，请访问其官方网站。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）
公众号二维码
公众号二维码
