7 hours ago
- 像Lean这样依赖类型的语言提供了强大的类型系统，但需要大量的证明工作，正如seL4项目所示，其证明代码量是实现代码的10倍以上。
- 大语言模型结合证明无关性（即证明的存在性才是关键）能够自动生成证明，使依赖类型在日常软件工程中更加实用。
- Zstandard是一种现代压缩工具，采用霍夫曼编码和有限状态熵编码（FSE）；FSE通过为常见符号分配多个状态实现了每符号分数比特的编码效率。
- Lean是一种严格纯函数式语言，支持引用计数为1时的可变性优化和命令式编程风格，适合性能敏感任务。
- 作者用Lean构建了Zstandard解压缩器，并利用大语言模型自动证明FSE表构造的属性，如表大小、状态计数及所有状态的可达性。