{"id":2426,"date":"2012-12-26T09:04:37","date_gmt":"2012-12-26T09:04:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2426"},"modified":"2016-10-16T12:24:15","modified_gmt":"2016-10-16T10:24:15","slug":"razonamiento-formalizado-del-sueno-a-la-realidad-de-las-pruebas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/razonamiento-formalizado-del-sueno-a-la-realidad-de-las-pruebas\/","title":{"rendered":"Razonamiento formalizado: Del sue\u00f1o a la realidad de las pruebas"},"content":{"rendered":"<p><a href=\"http:\/\/www.lifl.fr\/~delahaye\">Jean-Paul Delahaye<\/a> ha publicado en <a href=\"http:\/\/interstices.info\/index.jsp\">Interstices<\/a> un art\u00edculo panor\u00e1mico sobre razonamiento asistido por ordenador titulado <a href=\"http:\/\/interstices.info\/jcms\/int_63417\/du-reve-a-la-realite-des-preuves\">Du r\u00eave \u00e0 la r\u00e9alit\u00e9 des preuves<\/a>. Una <a href=\"http:\/\/www2.lifl.fr\/~delahaye\/IAGL\/AssistantPreuve.pdf\">versi\u00f3n anterior<\/a> de este trabajo se public\u00f3 en la revista <a href=\"http:\/\/www.pourlascience.fr\/\">Pour la Science<\/a>.<\/p>\n<p>El art\u00edculo comienza con una peque\u00f1a historia del razonamiento formalizado. Comienza con el <a href=\"http:\/\/www.rbjones.com\/rbjpub\/philos\/history\/xh003.html\">sue\u00f1o de Leibniz<\/a> en el siglo XVII de reducir el razonamiento al c\u00e1lculo. El sue\u00f1o fue parcialmente realizado por los <a href=\"http:\/\/es.wikipedia.org\/wiki\/Principia_mathematica\">Principia Mathematica<\/a> (1910-13) de Alfred Whitehead y Bertrand Russell en los que se intenta reducir las matem\u00e1ticas a la l\u00f3gica. En esta obra se muestra c\u00f3mo las matem\u00e1ticas pueden ser formalizables en teor\u00eda, pero no en la realidad (ya que la formalizaci\u00f3n que proponen es demasiado compleja para realizarla pr\u00e1cticamente). A este trabajo le han sucedido otras formalizaciones, como la de <a href=\"http:\/\/es.wikipedia.org\/wiki\/Nicolas_Bourbaki\">Bourbaki<\/a> en los a\u00f1os 30, basada en la teor\u00eda de conjuntos pero con parecidos inconvenientes.<\/p>\n<p>Sin embargo, la inform\u00e1tica y un siglo de trabajo de los l\u00f3gicos han hecho realidad el sue\u00f1o y logrado formalizaciones pr\u00e1cticas y reales de las matem\u00e1ticas. El primer trabajo de formalizaci\u00f3n de las matem\u00e1ticas fue el proyecto <a href=\"http:\/\/en.wikipedia.org\/wiki\/Automath\">Automath<\/a> desarrollado por <a href=\"http:\/\/en.wikipedia.org\/wiki\/Nicolaas_Govert_de_Bruijn\">Nicolaas de Bruijn<\/a> a partir de 1966. Su trabajo fue seguido por otros proyectos como <a href=\"http:\/\/en.wikipedia.org\/wiki\/Mizar_system\">Mizar<\/a>, <a href=\"http:\/\/en.wikipedia.org\/wiki\/HOL_%28proof_assistant%29\">HOL<\/a>, <a href=\"http:\/\/en.wikipedia.org\/wiki\/Isabelle_%28proof_assistant%29\">Isabelle<\/a> y <a href=\"http:\/\/en.wikipedia.org\/wiki\/Coq\">Coq<\/a>. La idea de estos asistentes de prueba es poner a disposici\u00f3n del usuario un sistema interactivo y un formalismo que le permita elaborar una versi\u00f3n formal de conomiento matem\u00e1tico.<\/p>\n<p>Una forma de mostrar el \u00e9xito obtenido con los asitentes de prueba en la formalizaci\u00f3n de las matem\u00e1ticas es comprobando las <a href=\"http:\/\/www.cs.ru.nl\/~freek\/100\/\">formalizaciones de los 100 principales teoremas<\/a> de la <a href=\"http:\/\/pirate.shu.edu\/~kahlnath\/Top100.html\">lista de Nathan Kahn<\/a>. Actualmente se ha formalizado el 87% de la lista entre los que destacan las demostraciones de<\/p>\n<ul>\n<li> la <a href=\"http:\/\/www.math.utah.edu\/~alfeld\/math\/q1.html\">irracionalidad de la raiz cuadradada de 2<\/a>,\n<li> la <a href=\"http:\/\/www.math.utah.edu\/~alfeld\/math\/q2.html\">infinitud de los n\u00fameros primos<\/a>,\n<li> la <a href=\"http:\/\/www.uwgb.edu\/dutchs\/PSEUDOSC\/trisect.HTM\">imposibilidad de la trisecci\u00f3n de un \u00e1ngulo<\/a>,\n<li> el <a href=\"http:\/\/mathworld.wolfram.com\/LagrangesFour-SquareTheorem.html\">teorema de Lagrange de los cuatro cuadro<\/a>\n<li> la <a href=\"http:\/\/www.jstor.org\/pss\/2690896\">f\u00f3rnula de Leibniz para \u03c0<\/a>: \u03c0\/4= 1 \u2013 1\/3 + 1\/5 \u2013 1\/7 + 1\/9 \u2013 &#8230;\n<li> la <a href=\"http:\/\/www.macalester.edu\/~bressoud\/talks\/mathfest2007\/harmonicproblems.pdf\">divergencia de la serie arm\u00f3nica<\/a>,\n<li> el <a href=\"http:\/\/www.cut-the-knot.com\/do_you_know\/fundamental2.shtml\">teorema fundamental del \u00e1lgebra<\/a>\n<li> el <a href=\"http:\/\/video.google.com\/videoplay?docid=4901007675211814617\">teorema fundamental del c\u00e1lculo integral<\/a>,\n<li> la <a href=\"http:\/\/planetmath.org\/EIsTranscendental.html\">transcendencia de e<\/a>,\n<li> el <a href=\"http:\/\/www4.ncsu.edu\/unity\/lockers\/users\/f\/felder\/public\/kenny\/papers\/godel.html\">primer teorema de incompletitud de G\u00f6del<\/a>,\n<li> el <a href=\"http:\/\/www.utm.edu\/research\/primes\/howmany.shtml\">teorema de los n\u00fameros primos<\/a> y\n<li> el <a href=\"http:\/\/www.npr.org\/templates\/story\/story.php?storyId=4254287&#038;ps=rs\">teorema de los cuatro colores<\/a>.\n<\/ul>\n<p>Algunos de los 13 teoremas de la listas pendientes de formalizar son<\/p>\n<ul>\n<li> <a href=\"http:\/\/en.wikipedia.org\/wiki\/Lindemann%E2%80%93Weierstrass_theorem\">la transcendencia del n\u00famero \u03c0<\/a>\n<li><a href=\"http:\/\/www.gap-system.org\/~history\/HistTopics\/Fermat%27s_last_theorem.html\">el teorema de Fermat-Wiles<\/a>.\n<\/ul>\n<p>Aparte de las anteriores formalizaciones de los anteriores teoremas, la utilidad de los asistentes de prueba se aprecia en los teoremas enormes como el de Thomas Hales que resuelve la conjetura de Kepler o el de clasificaci\u00f3n de los grupos simples.<\/p>\n<p>Otro campo de aplicaci\u00f3n de los asistentes de prueba se encuentra en la verificaci\u00f3n de programas y sistemas inform\u00e1ticos.<\/p>\n<p>A pesar de los \u00e9xitos obtenidos se plantean varios problemas como son:<\/p>\n<ul>\n<li> la confianza en la correcci\u00f3n en los propios asistentes de prueba. Se consigue aumentarla reduciendo el n\u00facleo del sistema a pocas l\u00edneas que sen simples y legibles, comprobando los n\u00facleos con numerosos ejemplos y demostrando la correci\u00f3n de los n\u00facleos con otros asistentes de prueba.\n<li> la dificultad del trabajo de formalizar (que se traduce en m\u00e1s de un d\u00eda de trabajo para formalizar una p\u00e1gina de texto matem\u00e1tico),\n<li> la escasa utilizaci\u00f3n de los asistentes en la investigaci\u00f3n matem\u00e1tica, aunque especialistas como Henk Barendregt y Freek Wiedijk vaticinan que en el pr\u00f3ximo decenio producir\u00e1n un cambio en los h\u00e1bitos de investigaci\u00f3n matem\u00e1tica.\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Jean-Paul Delahaye ha publicado en Interstices un art\u00edculo panor\u00e1mico sobre razonamiento asistido por ordenador titulado Du r\u00eave \u00e0 la r\u00e9alit\u00e9 des preuves. Una versi\u00f3n anterior de este trabajo se public\u00f3 en la revista Pour la Science. El art\u00edculo comienza con una peque\u00f1a historia del razonamiento formalizado. Comienza con el sue\u00f1o de Leibniz en el siglo&#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":[1],"tags":[166,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\/2426"}],"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=2426"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2426\/revisions"}],"predecessor-version":[{"id":5556,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2426\/revisions\/5556"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2426"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2426"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2426"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}