MechAlign：用 LLM 审查 Lean 数学形式化的项目级语义对齐

Lean 只能验证形式化证明在其声明假设下成立，无法判断命题是否忠实表达了论文中的数学断言。MechAlign 框架结合其提取工具 LeanTrace 构建语句依赖图，再由 LLM 在该上下文中检查对齐并给出带定位证据的差异报告。团队对来自 173 个 OpenAI Math 项目的 201 个主要结果做了初步审查，并以双曲群案例展示了依赖检查如何定位缺失的维度约束。论文同时发布了 LeanReviewBench，包含来自 OpenAI Math、Fermat's Last Theorem 和 Kakeya 的 501 个固定 claim-statement-context 三元组。