{"id":5218,"date":"2015-12-14T12:57:08","date_gmt":"2015-12-14T11:57:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5218"},"modified":"2015-12-14T12:57:08","modified_gmt":"2015-12-14T11:57:08","slug":"resena-formal-proofs-of-transcendence-for-e-and-%cf%80-as-an-application-of-multivariate-and-symmetric-polynomials","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-proofs-of-transcendence-for-e-and-%cf%80-as-an-application-of-multivariate-and-symmetric-polynomials\/","title":{"rendered":"Rese\u00f1a: Formal proofs of transcendence for e and \u03c0 as an application of multivariate and symmetric polynomials"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\">Coq<\/a> sobre teor\u00eda de n\u00fameros titulado <a href=\"http:\/\/arxiv.org\/pdf\/1512.02791v1\">Formal proofs of transcendence for e and \u03c0 as an application of multivariate and symmetric polynomials<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li>Sophie Bernard (del grupo <a href=\"http:\/\/www-sop.inria.fr\/marelle\/index.html\">Marelle<\/a> en  el <a href=\"http:\/\/www.inria.fr\/centre\/sophia\">Inria Sophia Antipolis &#8211; M\u00e9diterran\u00e9e<\/a>, Francia).<\/li>\n<li><a href=\"http:\/\/www-sop.inria.fr\/marelle\/Yves.Bertot\">Yves Bertot<\/a> (del grupo <a href=\"http:\/\/www-sop.inria.fr\/marelle\/index.html\">Marelle<\/a> en  el <a href=\"http:\/\/www.inria.fr\/centre\/sophia\">Inria Sophia Antipolis &#8211; M\u00e9diterran\u00e9e<\/a>, Francia),<\/li>\n<li><a href=\"https:\/\/www-sop.inria.fr\/members\/Laurence.Rideau\/moi.html\">Laurence Rideau<\/a> (del grupo <a href=\"http:\/\/www-sop.inria.fr\/marelle\/index.html\">Marelle<\/a> en  el <a href=\"http:\/\/www.inria.fr\/centre\/sophia\">Inria Sophia Antipolis &#8211; M\u00e9diterran\u00e9e<\/a>, Francia) y<\/li>\n<li><a href=\"http:\/\/www.strub.nu\">Pierre-Yves Strub<\/a> (del <a href=\"http:\/\/software.imdea.org\">Instituto IMDEA Software<\/a> en Madrid).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We describe the formalisation in Coq of a proof that the numbers e and \u03c0 are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of \u03c0 relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el 18 de enero de 2016 en el <a href=\"https:\/\/people.csail.mit.edu\/adamc\/cpp16\/\">CPP 2016<\/a> (<em>The 5th ACM SIGPLAN Conference on Certified Programs and Proofs<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/marelledocsgit.gforge.inria.fr\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre teor\u00eda de n\u00fameros titulado Formal proofs of transcendence for e and \u03c0 as an application of multivariate and symmetric polynomials. Sus autores son Sophie Bernard (del grupo Marelle en el Inria Sophia Antipolis &#8211; M\u00e9diterran\u00e9e, Francia). Yves Bertot (del grupo Marelle en el Inria&#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":[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\/5218"}],"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=5218"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5218\/revisions"}],"predecessor-version":[{"id":5219,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5218\/revisions\/5219"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5218"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5218"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5218"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}