LAX 发布：自然数学语言直连 Lean，可形式化复杂度类结果

lpachter · x · 2026-09-18

LAX 今日上线，是一个将自然数学语言与 Lean 定理证明器连接的工具，官方演示了用它定义复杂度类并形式化部分复杂度结果，例如非确定空间对补运算封闭。

不过 Lennart pachter 实验室作者 lpachter 评价称，该项目看起来精致实用，但与其开源工具 span 高度相似。span 的做法是：索引 Lean 4 声明、解析 LaTeX 论文的 \label 标记，用 JSON 账本（ledger）把论文对象与 Lean 声明对齐，记录每个对象由哪些声明实现、是否已形式化，并从标注的 LaTeX、Lean 源码和账本确定性地推导依赖图，同时提供 CLI 和 Python 库两种形态。这引出了数学形式化工具赛道同质化的问题。