Abstract: In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well. In this talk we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing the large corpus of Group Theory required by the Local Analysis part of the Odd Order Theorem.