ProofPatch: Reviewing Lean Statements and Keeping the Reviews Valid as Formalizations Evolve

Xujun Che, Depeng Xu, Jian Xiang +1

The kernel of the Lean proof assistant checks that a proof establishes its statement. Whether the statement says what was intended is left to human reviewers. This is the old probl…