{"id":432,"date":"2010-08-21T11:28:03","date_gmt":"2010-08-21T11:28:03","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-certified-proof-of-the-cartan-fixed-point-theorems\/"},"modified":"2013-03-08T05:53:42","modified_gmt":"2013-03-08T05:53:42","slug":"a-certified-proof-of-the-cartan-fixed-point-theorems","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-certified-proof-of-the-cartan-fixed-point-theorems\/","title":{"rendered":"Rese\u00f1a: A certified proof of the Cartan Fixed Point Theorems"},"content":{"rendered":"<p>\n<a href=\"http:\/\/web.math.unifi.it\/users\/ciolli\/\">Gianni Ciolli<\/a>, <a href=\"http:\/\/web.math.unifi.it\/users\/gentili\/\">Graziano Gentili<\/a> y <a href=\"http:\/\/web.math.unifi.it\/users\/maggesi\/\">Marco Maggesi<\/a> han publicado el art\u00edculo <a href=\"http:\/\/www.springerlink.com\/content\/w21219334v8m257h\/\">A Certified Proof of the Cartan Fixed Point Theorems<\/a> en el <a href=\"http:\/\/www.springerlink.com\/content\/0168-7433\/\">Journal of Automated Reasoning<\/a>. Una versi\u00f3n del art\u00edculo puede leerse <a href=\"https:\/\/neo.math.unifi.it\/users\/gentili\/lavoripdf\/cartan.pdf\">aqu\u00ed<\/a>.<\/p>\n<p>\nLos autores son profesores del <a href=\"http:\/\/www.math.unifi.it\/\">Departamento de Matem\u00e1ticas &#8220;Ulisses Dini&#8221;<\/a> de la Universidad de Florencia. Los dos primeros son especialistas en geometr\u00eda algebraica y an\u00e1lisis complejo y el tercero trabaja en razonamiento autom\u00e1tico con Coq y HOL Light.<\/p>\n<p>\nEl objetivo del art\u00edculo es la aplicaci\u00f3n del razonamiento formalizado a temas de investigaci\u00f3n de la matem\u00e1tica contempor\u00e1nea. Para ello han elegido como objetivo la formalizaci\u00f3n de los teoremas de Cartan del punto fijo, demostrados por <a href=\"http:\/\/en.wikipedia.org\/wiki\/Henri_Cartan\">Henri Cartan<\/a> en 1930. Los teoremas elegidos son relativamente recientes y de gran importancia en el an\u00e1lisis complejos y campos relacionados.<br \/>\n<!--more--><\/p>\n<p>\nLos teoremas del punto fijo de Cartan formalizados son los siguientes:<\/p>\n<ol>\n<li> (Primer teorema de Cartan) Sea <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=D+%5Csubseteq+%5Cmathbb%7BC%7D%5En&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"D &#92;subseteq &#92;mathbb{C}^n\" class=\"latex\" \/> un dominio acotado, <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=f%3A+D+%5Cto+D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"f: D &#92;to D\" class=\"latex\" \/> una funci\u00f3n holom\u00f3rfica y <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=z_0+%5Cin+D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"z_0 &#92;in D\" class=\"latex\" \/>. Si <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=f%28z_0%29%3Dz_0&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"f(z_0)=z_0\" class=\"latex\" \/> y el diferencial <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=df%28z_0%29&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"df(z_0)\" class=\"latex\" \/> de <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=f&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"f\" class=\"latex\" \/> en <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=z_0&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"z_0\" class=\"latex\" \/> es la funci\u00f3n identidad, entonces <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=f&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"f\" class=\"latex\" \/> es la funci\u00f3n identidad.\n<li> (Segundo teorema de Cartan) Sea <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=D+%5Csubseteq+%5Cmathbb%7BC%7D%5En&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"D &#92;subseteq &#92;mathbb{C}^n\" class=\"latex\" \/> un dominio acotado circular<br \/>\ncon <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=0+%5Cin+D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"0 &#92;in D\" class=\"latex\" \/> y <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=g&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"g\" class=\"latex\" \/> un automorfismo holom\u00f3rfico de <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"D\" class=\"latex\" \/> tal que <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=g%280%29%3D0&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"g(0)=0\" class=\"latex\" \/>. Entonces, <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=g&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"g\" class=\"latex\" \/> es la restricci\u00f3n a <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"D\" class=\"latex\" \/> de un automorfismo de <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=%5Cmathbb%7BC%7D%5En&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"&#92;mathbb{C}^n\" class=\"latex\" \/>.<\/p>\n<li> (Aplicaci\u00f3n del segundo teorema de Cardan) El grupo de todos los automorfismos holom\u00f3rficos de la bola abierta unidad de <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=%5Cmathbb%7BC%7D%5En&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"&#92;mathbb{C}^n\" class=\"latex\" \/> coincide con el grupo de todas las transformaciones de M\u00f6bius,\n<\/ol>\n<p>\nComo sistema para la formalizaci\u00f3n han elegido <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a> ya que cuenta con muchas teor\u00edas formalizadas para an\u00e1lisis complejo.<\/p>\n<p>Las teor\u00edas desarrolladas en Hol Light son:<\/p>\n<ul>\n<li> <a href=\"http:\/\/code.google.com\/p\/hol-light\/source\/browse\/trunk\/Library\/iter.ml\">Library\/iter.ml<\/a> para propiedades de la iteraci\u00f3n de aplicaciones de una funci\u00f3n;\n<li> <a href=\"http:\/\/code.google.com\/p\/hol-light\/source\/browse\/trunk\/Multivariate\/canal.ml\">Multivariate\/canal.ml<\/a> para los resultados sobre la analiticidad en el entorno de un punto;\n<li><a href=\"http:\/\/code.google.com\/p\/hol-light\/source\/browse\/trunk\/Multivariate\/cauchy.ml\">Multivariate\/cauchy.ml<\/a> para las demostraciones del primer y segundo teorema de Cardan;\n<li> <a href=\"http:\/\/code.google.com\/p\/hol-light\/source\/browse\/trunk\/Examples\/moebius.ml\">Examples\/moebius.ml<\/a> para las funciones de M\u00f6bius y la clasificaci\u00f3n de los automorfismos del disco unidad.\n<\/ul>\n<p>\nEn <a href=\"http:\/\/web.math.unifi.it\/users\/maggesi\/mechanized\/Cartan\/\">A Formalization of Cartan&#8217;s theorem in HOL<\/a> se encuentran todas las teor\u00edas juntas y un <a href=\"http:\/\/web.math.unifi.it\/users\/maggesi\/mechanized\/Cartan\/cartan.pdf\">esquema de la demostraci\u00f3n<\/a>.<\/p>\n<p>\nEntre las dificultades que comentan loa autores en la realizai\u00f3n de la formalizaci\u00f3n destacan los siguientes:<\/p>\n<ul>\n<li> La dificultad de comenzar a usar el sistema de razonamiento y de buscar los lemas adecuados para la demostraci\u00f3n. La existencia de gran cantidad de conocimiento formalizado es una facilidad pero su reutilizaci\u00f3n es dif\u00edcil, aunque la dificultad se ve aliviada con la ayuda del buscador de lemas que posee HOL Light.\n<li> El estilo de demostraci\u00f3n ha sido procedural en lugar de declarativo (como Mizar, Isar o C-zar) lo que dificulta la lectura de las pruebas por parte de las personas. Esta dificultad es especialmente notable en los casos de demostraci\u00f3n de resultados matem\u00e1ticos donde la prueba es tan interesante como el resultado que se demuestra.\n<\/ul>\n<p>\nLa formalizaci\u00f3n es compacta (con un factor de Bruijn de 3.5) y muesta la viabilidad de aplicar el razonamiento formalizado a teoremas importantes del an\u00e1lisis complejo. y puede continuarse formalizando otros rsultados del an\u00e1lisis complejo.<\/p>\n<p>\nFinalmente, me parece una idea interesante la formalizaci\u00f3n de resultados matem\u00e1ticos importantes y relativamente recientes (por ejemplo, los demostrados en el siglo XX). Comenzar\u00e9 su elaboraci\u00f3n en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/los-principales-teoremas-del-siglo-xx-y-su-formalizacion\/\">siguiente entrada<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Gianni Ciolli, Graziano Gentili y Marco Maggesi han publicado el art\u00edculo A Certified Proof of the Cartan Fixed Point Theorems en el Journal of Automated Reasoning. Una versi\u00f3n del art\u00edculo puede leerse aqu\u00ed. Los autores son profesores del Departamento de Matem\u00e1ticas &#8220;Ulisses Dini&#8221; de la Universidad de Florencia. Los dos primeros son especialistas en geometr\u00eda&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","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":[99,89,22],"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\/432"}],"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=432"}],"version-history":[{"count":16,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/432\/revisions"}],"predecessor-version":[{"id":3034,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/432\/revisions\/3034"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=432"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=432"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=432"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}