This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed a comprehensive set of reusable libraries of formalized mathematics, including results in finite group theory, linear algebra, Galois theory, and the theories of the real and complex algebraic numbers.<\/p>\n","protected":false},"excerpt":{"rendered":"
This paper reports on a six-year collaborative effort that culminated in a complete formalization of a proof of the Feit-Thompson Odd Order Theorem in the Coq proof assistant. The formalized proof is constructive, and relies on nothing but the axioms and rules of the foundational framework implemented by Coq. To support the formalization, we developed […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_publishername":"Springer, Berlin, Heidelberg","msr_publisher_other":"","msr_booktitle":"","msr_chapter":"","msr_edition":"","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"","msr_page_range_start":"163","msr_page_range_end":"179","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"Interactive Theorem Proving","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"1768814311","msr_pubmed_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2013-7-22","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":0,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13563],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[250642,250618,250639,250630,249139,250624,250633,250636,250621,250627],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-720412","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-data-platform-analytics","msr-locale-en_us","msr-field-of-study-algebra","msr-field-of-study-analytic-proof","msr-field-of-study-computer-assisted-proof","msr-field-of-study-constructive-proof","msr-field-of-study-discrete-mathematics","msr-field-of-study-mathematical-proof","msr-field-of-study-proof-assistant","msr-field-of-study-proof-by-contradiction","msr-field-of-study-proof-theory","msr-field-of-study-structural-proof-theory"],"msr_publishername":"Springer, Berlin, Heidelberg","msr_edition":"","msr_affiliation":"","msr_published_date":"2013-7-22","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"doi","viewUrl":"false","id":"false","title":"10.1007\/978-3-642-39634-2_14","label_id":"243106","label":0},{"type":"url","viewUrl":"false","id":"false","title":"http:\/\/www.cs.unibo.it\/~asperti\/PAPERS\/odd_order.pdf","label_id":"243132","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/hal.inria.fr\/hal-00816699\/file\/main.pdf","label_id":"243132","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/core.ac.uk\/display\/102759416","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/dblp.uni-trier.de\/db\/conf\/itp\/itp2013.html#GonthierAABCGRMOBPRSTT13","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/hal.archives-ouvertes.fr\/hal-00816699v1","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/hal.inria.fr\/hal-00816699","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-642-39634-2_14","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/philpapers.org\/rec\/GONAMP","label_id":"243109","label":0},{"type":"url","viewUrl":"false","id":"false","title":"https:\/\/rd.springer.com\/chapter\/10.1007\/978-3-642-39634-2_14","label_id":"243109","label":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[],"msr-author-ordering":[{"type":"text","value":"Georges Gonthier","user_id":0,"rest_url":false},{"type":"text","value":"Andrea Asperti","user_id":0,"rest_url":false},{"type":"text","value":"Jeremy Avigad","user_id":0,"rest_url":false},{"type":"text","value":"Yves Bertot","user_id":0,"rest_url":false},{"type":"text","value":"Cyril Cohen","user_id":0,"rest_url":false},{"type":"text","value":"Fran\u00e7ois Garillot","user_id":0,"rest_url":false},{"type":"text","value":"St\u00e9phane Le Roux","user_id":0,"rest_url":false},{"type":"text","value":"Assia Mahboubi","user_id":0,"rest_url":false},{"type":"text","value":"Russell O'Connor","user_id":0,"rest_url":false},{"type":"text","value":"Sidi Ould Biha","user_id":0,"rest_url":false},{"type":"text","value":"Ioana Pasca","user_id":0,"rest_url":false},{"type":"text","value":"Laurence Rideau","user_id":0,"rest_url":false},{"type":"text","value":"Alexey Solovyev","user_id":0,"rest_url":false},{"type":"text","value":"Enrico Tassi","user_id":0,"rest_url":false},{"type":"text","value":"Laurent Th\u00e9ry","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[663087],"msr_project":[],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/720412","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/720412\/revisions"}],"predecessor-version":[{"id":721657,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/720412\/revisions\/721657"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=720412"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=720412"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=720412"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=720412"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=720412"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=720412"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=720412"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=720412"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=720412"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=720412"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=720412"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=720412"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=720412"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}