I am sitting in Tom Hales Talk at MKM 2007, where he discusses how he is re-arranging his 1998 proof of the Kepler conjecture in a way so that it becomes more palatable to formalization process (the flyspeck project). He says that the proof text is becoming much less dense in the process.
This seems like a very good case study for MKM, most particular the SWIM semantic Wiki for Math, together with Normen’s Change managment techniques (see Locutor).
I think that I will ask him for access to the text as a case study.