Polish Salamucha's Formalization
I think the following things need to be done to make Salamucha's formalization more "presentable":
-
There are many typos in the text and in comments that need to be fixed.
-
We need to follow a policy about when to use "text" and when to use Isabelle comments. I suggest that "text" be used for general discussion about the argument itself, whereas Isabelle comments be used for technical remarks (e.g. whether this or that prover succeeded or failed, and so on...)
-
Salamucha's natural language statements should be included (as "text") before every definition, abbreviation, lemma and theorem.
-
The file is currently very long. We should split it. I propose the following: everything that is strictly a formalization of Salamucha's argument should be in one file; any other investigation that you did in addition to what Salamucha claimed should be in another file.