ProofPatch：在形式化演进中审查 Lean 陈述并保持审查有效

ProofPatch 工具可帮助审查者判断 Lean 陈述是否符合本意，并在形式化开发变化时保持审查结论有效。它基于 Lean 展开后的项而非源文本记录审查决定，在 Mathlib 的 229 对连续修订中仅将 12,898 条合成决定中的 118 条送回审查，而所有基于文本的替代方案至少漏掉 38 条或多送回 13 倍。