Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ...
by alexpeattie on Tuesday December 05, 2023 @05:14PM
(#38537686)
The proof text is separate. Currently it's up to humans to ensure the proof text (written in LaTeX) properly matches the Lean proof.
Indeed, you can see in the article that the text of Theorem 7.2 omits for brevity details which are present in the non-pretty printed Lean proof (for example H is non-empty, K is a real number, etc.)
Indeed, you can see in the article that the text of Theorem 7.2 omits for brevity details which are present in the non-pretty printed Lean proof (for example H is non-empty, K is a real number, etc.)