Engineering Mathematics: The Odd Order Theorem Proof

摘要

Even with the assistance of computer tools, the formalized description and verification of research-level mathematics remains a daunting task, not least because of the talent with which mathematicians combine diverse theories to achieve their ends. By combining tools and techniques from type theory, language design, and software engineering we have managed to capture enough of these practices to formalize the proof of the Odd Order theorem, a landmark result in Group Theory.