AI正重塑全球软件开发，但高质量代码稀缺。通过Lean平台进行数学验证，能为AI生成的复杂系统提供可靠性保障，将开发重心转向精准的设计规约。
数字世界正在被重新编写。Code Metal筹集了1.25亿美元用于重写国防软件，微软和谷歌报告称其25%至30%的新代码由AI生成。微软的首席技术官甚至预测，到2030年，95%的代码将由AI产出。然而，在这场效率狂欢背后，一个巨大的鸿沟正在裂开，那就是验证。
目前的现状令人担忧。正如Andrej Karpathy所观察到的，当AI生成的代码在大部分时间里看起来“还不错”时，人类工程师就开始习惯性地点击“全部接受”。哈佛商业评论将这种现象称为“工作废料”，即那些外表华丽但内部逻辑千疮百孔的AI作品。当这些废料出现在备忘录中只是让人烦恼，但如果出现在加密库里，那就是灾难。历史上一个微小的漏洞Heartbleed就曾让数百万用户的私密通信曝光，即便经过数年的代码审查也未能被发现。如今AI产出代码的速度是人类的1000倍，这意味着错误出现的频率和规模也将以千倍速扩张。
传统的测试和人工审查已经捉襟见肘。我们需要的是数学证明。测试只能提供信心，而证明能提供百分之百的保证。亚马逊云科技的应用科学家、Lean平台首席架构师Leonardo de Moura认为，解决办法不是让AI慢下来，而是引入“数学摩擦”。这意味着我们要让AI在快速生成代码的同时，必须证明其工作的正确性。
Lean平台已经成为这一变革的核心。它既是一种编程语言，也是一种定理证明器。目前，谷歌深思维、字节跳动、安斯罗皮克等巨头的AI推理系统都在使用它。通过Lean，我们可以为复杂的软件建立数学模型。当AI生成一段代码时，Lean的内核会像严厉的考官一样，从数学层面检查每一个逻辑步骤，确保它在所有可能的输入下都运行正确。
最近的一项实验展示了这种力量。研究人员利用安斯罗皮克公司的Claude模型，在极少的人工引导下，将广泛使用的压缩库zlib转换成了Lean版本，并生成了机器可检查的数学证明。这证明了即使是通用的AI，在合适的平台上也能产出经过严格验证的高质量软件。这在过去被认为是不可能完成的任务。
随着AI接管具体的代码编写，工程师的角色也将发生根本性转变。未来的核心技能不再是埋头于复杂的实现细节，而是编写精准的“规约”，即定义一个系统究竟什么是正确的。这要求工程师进行更深层次的设计思考，而非机械的录入。
这场变革的终极目标是建立一个“验证堆栈”。从基础的加密算法到像SQLite这样的存储引擎，全部由数学逻辑守卫。这种验证过的开源组件将成为永久的公共利益，任何人都可以审计和信任。当正确性的成本降到几乎为零时，航空航天、医疗设备和金融系统的安全性将迎来质的飞跃。在这个AI编写软件的新时代，数学证明将是我们数字文明最后的安全底线。
本文译自 leodemoura，由 BALI 编辑发布。
