论文Agent 与开发者多源确认12:12MechAlign：用 LLM 审查 Lean 数学形式化的项目级语义对齐有人给 Lean 形式化做了个语义对齐检查器，用依赖图让 LLM 找形式化定理和论文原文的出入，还放了个 501 条的基准。#MechAlign#Lean#LeanReviewBench#形式化验证10 个信源在谈事件专题aarXiv: OpenAI@Hao Shen 等 4 人11 个信源在谈原文稍后读已读值得跟进有用关注 MechAlign