{"id":3272,"date":"2013-04-29T06:16:35","date_gmt":"2013-04-29T06:16:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3272"},"modified":"2013-04-29T07:45:44","modified_gmt":"2013-04-29T07:45:44","slug":"a-machine-checked-proof-of-the-odd-order-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-machine-checked-proof-of-the-odd-order-theorem\/","title":{"rendered":"Rese\u00f1a: A machine-checked proof of the odd order theorem"},"content":{"rendered":"

Una de las l\u00edneas de trabajo en la automatizaci\u00f3n del razonamiento es la verificaci\u00f3n de demostraciones de grandes teoremas. En esta l\u00ednea se inscribe el proyecto de la formalizaci\u00f3n en Coq<\/a> del teorema clasificaci\u00f3n de grupos finitos<\/a>. Un resultado clave para dicha demostraci\u00f3n es el teorema de Feit y Thompson<\/a>, tambi\u00e9n conocido como el teorema del orden impar. Recientemente se ha conseguido la formalizaci\u00f3n del teorema en Coq como se comenta en el art\u00edculo A machine-checked proof of the odd order theorem<\/a>.<\/p>\n

Sus autores son Georges Gonthier<\/a>, Andrea Asperti<\/a>, Jeremy Avigad<\/a>, Yves Bertot<\/a>, Cyril Cohen<\/a>, Fran\u00e7ois Garillot<\/a>, St\u00e9phane Le Roux<\/a>, Assia Mahboubi<\/a>, Russell O\u2019Connor<\/a>, Sidi Ould Biha<\/a>, Ioana Pasca<\/a>, Laurence Rideau<\/a>, Alexey Solovyev<\/a>, Enrico Tassi<\/a> y Laurent Th\u00e9ry<\/a>.<\/p>\n

Su resumen es<\/p>\n

\nThis 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.\n<\/p><\/blockquote>\n

Las conclusiones del trabajo son<\/p>\n

\nThe success of the present formalization relies on a heavy use of the inductive types provided by Coq and on various flavors of reflection techniques. A crucial ingredient was the transfer of the methodology of \u201cgeneric programming\u201d to formal proofs, using the type inference mechanisms of the Coq system. <\/p>\n

Our development includes more than 150,000 lines of proof scripts, including roughly 4,000 definitions and 13,000 theorems. The roughly 250 pages of mathematics in our two main sources translate to about 40,000 lines of formal proof, which amounts to 4-5 lines of SSReflect code per line of informal text. During the formalization, we had to correct or rephrase a few arguments in the texts we were following, but the most time-consuming part of the project involved getting the base and intermediate libraries right. This required systematic consolidation phases performed after the production of new material. The corpus of mathematical theories preliminary to the actual proof of the Odd Order theorem represents the main reusable part of this work, and contributes to almost 80 percent of the total length. Of course, the success of such a large formalization, involving several people at different locations, required a very strict discipline, with uniform naming conventions, synchronization of parallel developments, refactoring, and benchmarking for synchronization with Coq. <\/p>\n

As we have tried to make clear in this paper, when it comes to formalizing this amount of mathematics, there is no silver bullet. But the combined success of the many techniques we have developed shows that we are now ready for theorem proving in the large. The outcome is not only a proof of the Odd Order Theorem, but also, more importantly, a substantial library of mathematical components, and a tried and tested methodology that will support future formalization efforts.\n<\/p><\/blockquote>\n

Una vesi\u00f3n minimal de la demostraci\u00f3n en Coq del teorema del orden impar se encuentra aqu\u00ed<\/a>. La formalizaci\u00f3n completa se encuentra aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

Una de las l\u00edneas de trabajo en la automatizaci\u00f3n del razonamiento es la verificaci\u00f3n de demostraciones de grandes teoremas. En esta l\u00ednea se inscribe el proyecto de la formalizaci\u00f3n en Coq del teorema clasificaci\u00f3n de grupos finitos. Un resultado clave para dicha demostraci\u00f3n es el teorema de Feit y Thompson, tambi\u00e9n conocido como el teorema…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3272"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3272"}],"version-history":[{"count":9,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3272\/revisions"}],"predecessor-version":[{"id":3281,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3272\/revisions\/3281"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3272"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3272"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3272"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}