|
|
|
|
|
|
by alexpeattie
930 days ago
|
|
|
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.) |
|
|