{"id":448,"date":"2010-08-22T07:33:10","date_gmt":"2010-08-22T07:33:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/los-principales-teoremas-del-siglo-xx-y-su-formalizacion\/"},"modified":"2013-03-08T05:53:42","modified_gmt":"2013-03-08T05:53:42","slug":"los-principales-teoremas-del-siglo-xx-y-su-formalizacion","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/los-principales-teoremas-del-siglo-xx-y-su-formalizacion\/","title":{"rendered":"Los principales teoremas del siglo XX y su formalizaci\u00f3n"},"content":{"rendered":"<p>\nComo comentaba en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-certified-proof-of-the-cartan-fixed-point-theorems\">entrada anterior<\/a>, un gran reto para el razonamiento formalizado podr\u00eda consistir en la formalizaci\u00f3n de los principales teoremas del siglo XX. <\/p>\n<p>\nEste reto es an\u00e1logo a <a href=\"http:\/\/www.cs.ru.nl\/~freek\/100\/\">Formalizing 100 Theorems<\/a> que consiste en la formalizaci\u00f3n de <a href=\"http:\/\/web.archive.org\/web\/20080105074243\/http:\/\/personal.stevens.edu\/~nkahl\/Top100Theorems.html\">los 100 principales teoremas de todos los tiempos<\/a>.<\/p>\n<p>\nEl punto de partida ha de ser la determinaci\u00f3n de cu\u00e1les son los principales teoremas del siglo XX y en qu\u00e9 punto se encuentra su formalizaci\u00f3n. <\/p>\n<p>\nAlgunos candidadatos de la lista de los principales teoremas del siglo XX son<br \/>\n<!--more--><\/p>\n<ul>\n<li> 1910: La demostraci\u00f3n de Brouwer del <a href=\"\">teorema del punto fijo<\/a>. Est\u00e1 formalizado en HOL Light (por John Harrison), en Mizar (por Artur Korni\u0142owicz y Yasunari Shidama) y en Isabelle (por Robert Himmelmann).\n<li> 1928: La demostraci\u00f3n de John von Neumann del <a href=\"http:\/\/en.wikipedia.org\/wiki\/Minimax_theorem#Minimax_theorem\">teorema minimax<\/a>.\n<li> 1930: La demostraci\u00f3n de Casimir Kuratowski de inexistencia de soluci\u00f3n del <a href=\"http:\/\/en.wikipedia.org\/wiki\/Three-cottage_problem\">problema de las tres casas<\/a>.\n<li> 1930: La demostraci\u00f3n del <a href=\"http:\/\/en.wikipedia.org\/wiki\/Ramsey's_theorem\">teorema de Ramsey<\/a>. Est\u00e1 formalizado en HOL Light (por John Harrison), en Mizar (por Marco Riccardi), en Isabelle (por Tom Ridge), en ProofPower (por Rob Arthan y Roger Bishop Jones), en PVS (por Natarajan Shankar), en Nqthm (por Matt Kaufmann) y en NuPRL (por David Basin).\n<li> 1931: La demostraci\u00f3n de Kurt G\u00f6del de los <a href=\"http:\/\/en.wikipedia.org\/wiki\/G%C3%B6del's_incompleteness_theorems\">teoremas de incompletitud<\/a>. Est\u00e1 formalizado en HOL Light (por John Harrison), en Coq (por Russell O&#8217;Connor) y en Nqthm (por Natarajan Shankar).\n<li> 1963: La demostraci\u00f3n de Paul Cohen de la <a href=\"\">indecidibilidad de la hip\u00f3tesis del continuo<\/a>\n<li> 1966: demostraci\u00f3n de Paul Erdos, Alfred Renyi y Vera Sos del <a href=\"http:\/\/en.wikipedia.org\/wiki\/Friendship_graph\">teorema de la amistad<\/a>. Est\u00e1 formalizado en HOL Light (por John Harrison).\n<li> 1976: La demostraci\u00f3n de Kenneth Appel y Wolfgang Haken de 1976 del <a href=\"http:\/\/en.wikipedia.org\/wiki\/Four_color_theorem\">teorema de los cuatros colores<\/a>. En 2005 Benjamin Werner y Georges Gonthier formalizaron una <a href=\"http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf\">demostraci\u00f3n del teorema en Coq<\/a>.\n<li> 1983: <a href=\"http:\/\/en.wikipedia.org\/wiki\/Classification_of_finite_simple_groups\">La clasificaci\u00f3n de los grupos finitos<\/a>. Su formalizaci\u00f3n se est\u00e1 realizando en el proyecto <a href=\"http:\/\/www.msr-inria.inria.fr\/Projects\/math-components\">Mathematical Components<\/a>. El estado de la formalizaci\u00f3n puede consultarse en <a href=\"http:\/\/coqfinitgroup.gforge.inria.fr\/\">Mathematical Component: Group Theory<\/a>.\n<li> 1993: La demostraci\u00f3n de <a href=\"http:\/\/es.wikipedia.org\/wiki\/Andrew_Wiles\">Andrew Wiles<\/a> del <a href=\"http:\/\/es.wikipedia.org\/wiki\/%C3%9Altimo_teorema_de_Fermat\">\u00faltimo teorema de Fermat<\/a>, que se coment\u00f3 en la entrada <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/reto-de-formalizacion-el-proyecto-wiles-fermat\/\"> Reto de formalizaci\u00f3n: El proyecto Wiles-Fermat<\/a>.\n<li> 1998: La demostraci\u00f3n de Thomas C. Hales de la <a href=\"http:\/\/en.wikipedia.org\/wiki\/Kepler_conjecture\">conjetura de Kepler<\/a>. Su formalizaci\u00f3n se est\u00e1 realizando dentro del <a href=\"http:\/\/code.google.com\/p\/flyspeck\/wiki\/FlyspeckFactSheet\">proyecto Flyspeck<\/a>.\n<\/ul>\n<p>\nM\u00e1s candidatos pueden extraerse de las siguientes referencias:<\/p>\n<ul>\n<li> <a href=\"http:\/\/en.wikipedia.org\/wiki\/Timeline_of_mathematics#20th_century\">Timeline of mathematics (20th century)<\/a>\n<li> <a href=\"http:\/\/aportes.educ.ar\/matematica\/nucleo-teorico\/estado-del-arte\/los-principales-hitos-de-la-matematica-en-el-siglo-xx\/algunos_descubrimientos_y_acon.php\">Algunos descubrimientos y acontecimientos destacables de la matem\u00e1tica del siglo XX<\/a>\n<li> <a href=\"http:\/\/aportes.educ.ar\/matematica\/nucleo-teorico\/estado-del-arte\/los-principales-hitos-de-la-matematica-en-el-siglo-xx\/algunos_de_los_avances_mas_imp.php\">Algunos de los avances m\u00e1s importantes en la matem\u00e1tica del siglo XX<\/a>.\n<li> <a href=\"http:\/\/books.google.es\/books?id=zv8UJdONFpcC&#038;printsec=frontcover#v=onepage&#038;q&#038;f=false\">La matem\u00e1tica del siglo XX<\/a>.\n<\/ul>\n<p>\n\u00bfCu\u00e1les son vuestros candidatos para la lista de los principales teoremas del siglo XX?   <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Como comentaba en la entrada anterior, un gran reto para el razonamiento formalizado podr\u00eda consistir en la formalizaci\u00f3n de los principales teoremas del siglo XX. Este reto es an\u00e1logo a Formalizing 100 Theorems que consiste en la formalizaci\u00f3n de los 100 principales teoremas de todos los tiempos. El punto de partida ha de ser la&#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":[8],"tags":[273,9],"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\/448"}],"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=448"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/448\/revisions"}],"predecessor-version":[{"id":3033,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/448\/revisions\/3033"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=448"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=448"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=448"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}