LAX 发布：自然语言数学直连 Lean 证明器

工具 LAX 正式上线，提供将自然数学语言与 Lean 定理证明器连接的方式，内置定义复杂度类的机制。官方演示了形式化复杂度理论结果，例如已归档的 Immerman–Szelepcsényi 定理（NL=coNL），即非确定空间对补运算封闭。不过形式化数学社区成员 Lennart 等人也提出了相关讨论。

2026-09-17 ~ 2026-09-18 · 2 条相关