The role of the Coq formalization

[ppolesiuk]

Two lectures are already formalized in Coq and I expect that more of them will be formalized too, but not all of them. How should we treat this formalization? Should we treat it as some useful resource loosely connected with the notes, or as an integral part of them? For definitions and theorems in the notes we can add pointers to corresponding counterparts in the formalization. I leave these ideas here and hope for some insightful comments.