亚马逊宣布将为Lean专项研究组织（Lean Focused Research Organization，简称Lean FRO）提供长期资金支持，以推动Lean编程语言的持续发展。Lean是一种能够对软件正确性进行数学证明的编程语言，在软件形式化验证领域具有重要价值。
目前，亚马逊已在多款产品中引入基于Lean的形式化验证技术。在智能体安全方面，Bedrock AgentCore采用该技术对智能体行为进行安全性验证；SampCert项目借助Lean为差分隐私保护提供数学层面的可靠性保证；AWS Neuron则将其应用于AI芯片编译流程的正确性验证。此外，亚马逊科学家正在探索大语言模型与Lean相结合的方式，用于证明复杂分布式协议的正确性。
值得关注的是，亚马逊选择通过独立机构Lean FRO来支持这一技术的发展，而非将其纳入内部研发体系。这一决策背后有明确的战略考量：保持工具的中立性与可信度，使客户、审计方和监管机构能够对相关证明工具进行独立验证，从而满足安全关键型AI应用在合规与透明度方面的高标准要求。
Q&A
Q1：Lean编程语言是什么？它在软件开发中有什么作用？
A：Lean是一种支持数学形式化证明的编程语言，能够从数学层面严格验证软件行为的正确性。与传统测试方法不同，Lean通过构建数学证明来保证软件在所有情况下均符合预期行为，特别适用于对安全性和可靠性要求极高的系统，如AI芯片编译、隐私保护算法等场景。
Q2：亚马逊为什么选择支持Lean FRO而不是在内部自行研发？
A：亚马逊将支持工作交由独立机构Lean FRO来承担，主要是为了保证验证工具的透明度与中立性。如果工具由亚马逊内部开发和维护，外部审计方和监管机构可能难以对其进行独立核查。通过支持独立组织，亚马逊的客户、第三方审计机构以及监管机构可以自主验证相关证明工具的可靠性，更好地满足安全关键型AI应用的合规需求。
Q3：大语言模型和Lean结合起来能做什么？
A：亚马逊科学家正在探索将大语言模型与Lean结合使用，目标是借助大语言模型的推理能力辅助生成形式化证明，用于验证复杂分布式协议的正确性。这类协议通常逻辑复杂、边界情况繁多，传统人工证明成本极高，大语言模型与Lean的组合有望大幅降低这一过程的难度和时间成本。
