{"id":6957,"date":"2020-01-25T21:15:26","date_gmt":"2020-01-25T20:15:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6957"},"modified":"2020-01-25T21:15:26","modified_gmt":"2020-01-25T20:15:26","slug":"resena-a-formal-proof-of-the-irrationality-of-%ce%b63","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-formal-proof-of-the-irrationality-of-%ce%b63\/","title":{"rendered":"Rese\u00f1a: A formal proof of the irrationality of \u03b6(3)"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado sobre teor\u00eda de n\u00fameros titulado <a href=\"https:\/\/arxiv.org\/abs\/1912.06611\">A formal proof of the irrationality of \u03b6(3)<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/people.rennes.inria.fr\/Assia.Mahboubi\/\">Assia Mahboubi<\/a> (del grupo <a href=\"http:\/\/gallinette.inria.fr\/\">Gallinette<\/a> en el <a href=\"http:\/\/www.inria.fr\/\">Inria<\/a>) y<\/li>\n<li><a href=\"https:\/\/specfun.inria.fr\/~tsibutpi\/\">Thomas Sibut-Pinote<\/a> (del <a href=\"https:\/\/specfun.inria.fr\/\">INRIA Team SpecFun<\/a> y la <i>Universit\u00e9 Paris-Saclay<\/i>)<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Ap\u00e9ry in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"https:\/\/github.com\/math-comp\/apery\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado sobre teor\u00eda de n\u00fameros titulado A formal proof of the irrationality of \u03b6(3). Sus autores son Assia Mahboubi (del grupo Gallinette en el Inria) y Thomas Sibut-Pinote (del INRIA Team SpecFun y la Universit\u00e9 Paris-Saclay) Su resumen es This paper presents a complete formal verification of a&#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":[],"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\/6957"}],"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=6957"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6957\/revisions"}],"predecessor-version":[{"id":6958,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6957\/revisions\/6958"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6957"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6957"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6957"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}