Lean 4 软件扩展定律
本文探讨了 Lean 4 编程语言和定理证明器在大规模软件工程中的扩展性规律。通过分析 Lean 4 在不同规模项目中的表现，作者总结了代码库规模增长时性能、编译时间和证明效率的变化趋势，并提出了适用于 Lean 4 的软件扩展定律，为形式化验证项目的规模化管理提供了指导。
背景速读
- Gwern是一个独立的研究者，长期研究深度学习scaling laws（规模缩放规律）——即模型性能随计算量、数据量和参数量的增长而稳定提升的现象。本文将其思路应用于软件工程领域。
- Lean 4是微软研究院与卡内基梅隆大学共同开发的形式化证明助手，可用来写数学证明的正确性验证。它具有严格的操作语义，比C/Rust/Python更可控、可测。
- 本文核心问题是：给Lean编译器更多资源（CPU时间、内存、优化努力），编译后的代码性能是否会稳定提升？结果发现确实存在类似深度学习的"编译scaling law"——资源投入越多，生成代码越快，且呈幂律关系。
- 意义：如果这一规律普遍成立，意味着编译器不再是"一次优化，永远最优"，而是一个可以靠不断加算力来持续改进的系统——这对编译器设计、硬件加速、甚至整个软件生态有深远影响。