{"id":2254,"date":"2012-10-26T04:46:45","date_gmt":"2012-10-26T04:46:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2254"},"modified":"2013-03-08T05:44:26","modified_gmt":"2013-03-08T05:44:26","slug":"a-string-of-pearls-proofs-of-fermat%e2%80%99s-little-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-string-of-pearls-proofs-of-fermat%e2%80%99s-little-theorem\/","title":{"rendered":"Rese\u00f1a: A string of pearls: Proofs of Fermat\u2019s little theorem"},"content":{"rendered":"<p>En la <a href=\"http:\/\/cpp12.kuis.kyoto-u.ac.jp\/\">CPP12<\/a> (<i>The Second International Conference on Certified Programs and Proofs<\/i>), que comienza el 13 de diciembre, se presentar\u00e1 un trabajo de razonamiento formalizado en <a href=\"http:\/\/hol.sourceforge.net\/\">HOL4<\/a> titulado <a href=\"http:\/\/www.nicta.com.au\/pub?doc=6061\">A string of pearls: Proofs of Fermat\u2019s little theorem<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/people.cecs.anu.edu.au\/user\/4798\">Hing-Lun Chan<\/a> (de la <i>Australian National University<\/i>) y <a href=\"http:\/\/www.nicta.com.au\/people\/norrishm\">Michael Norrish<\/a> (del <i>Canberra Research Lab., NICTA<\/i>).<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nWe discuss mechanised proofs of <a href=\"http:\/\/en.wikipedia.org\/wiki\/Fermat%27s_little_theorem\">Fermat\u2019s Little Theorem<\/a> in a variety of styles, focusing in particular on <a href=\"http:\/\/en.wikipedia.org\/wiki\/Proofs_of_Fermat%27s_little_theorem#Proof_by_counting_necklaces\">an elegant combinatorial &#8220;necklace&#8221; proof<\/a> that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for the direct number-theoretic approach.\n<\/p><\/blockquote>\n<p>El c\u00f3digo conteniendo las demostraciones en HOL4 se encuentra <a href=\"http:\/\/bitbucket.org\/jhlchan\/hol\/src\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la CPP12 (The Second International Conference on Certified Programs and Proofs), que comienza el 13 de diciembre, se presentar\u00e1 un trabajo de razonamiento formalizado en HOL4 titulado A string of pearls: Proofs of Fermat\u2019s little theorem. Sus autores son Hing-Lun Chan (de la Australian National University) y Michael Norrish (del Canberra Research Lab., NICTA)&#8230;.<\/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":[100,1],"tags":[199,273,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\/2254"}],"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=2254"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2254\/revisions"}],"predecessor-version":[{"id":2644,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2254\/revisions\/2644"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2254"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2254"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2254"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}