{"id":5459,"date":"2016-07-28T11:03:20","date_gmt":"2016-07-28T09:03:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5459"},"modified":"2016-07-28T11:03:20","modified_gmt":"2016-07-28T09:03:20","slug":"resena-a-formally-verified-proof-of-the-central-limit-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-formally-verified-proof-of-the-central-limit-theorem\/","title":{"rendered":"Rese\u00f1a: A formally verified proof of the central limit theorem"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre probabilidad titulado <a href=\"http:\/\/arxiv.org\/pdf\/1405.7012v2\">A formally verified proof of the central limit theorem<\/a><\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\">Jeremy Avigad<\/a> (de la <em>Carnegie Mellon University<\/em>), <\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~hoelzl\">Johannes H\u00f6lzl<\/a> (del grupo <a href=\"http:\/\/www21.in.tum.de\/\">Logic and Verification<\/a> de la <em>TU M\u00fcnchen<\/em>) y <\/li>\n<li>Luke Serafin (de la <em>Carnegie Mellon University<\/em>).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle&#8217;s libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"https:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-Probability\/Central_Limit_Theorem.html\">aqu\u00ed<\/a> dentro del desarrollo de la <a href=\"https:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-Probability\/document.pdf\">teor\u00eda de la probabilidad<\/a>.<\/p>\n<p>Este art\u00edculo puede servir de lectura complementaria en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a>, <a href=\"http:\/\/www.cs.us.es\/cursos\/rac\/\">Razonamiento asistido por ordenador<\/a> y <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/LCyTM-15\">L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre probabilidad titulado A formally verified proof of the central limit theorem Sus autores son Jeremy Avigad (de la Carnegie Mellon University), Johannes H\u00f6lzl (del grupo Logic and Verification de la TU M\u00fcnchen) y Luke Serafin (de la Carnegie Mellon University). Su resumen es We&#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],"tags":[144,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\/5459"}],"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=5459"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5459\/revisions"}],"predecessor-version":[{"id":5460,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5459\/revisions\/5460"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5459"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5459"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5459"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}