{"id":1133,"date":"2011-01-09T06:51:13","date_gmt":"2011-01-09T06:51:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1133"},"modified":"2013-03-08T05:50:04","modified_gmt":"2013-03-08T05:50:04","slug":"proofwiki-y-la-verificacion-de-las-demostraciones-matematicas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proofwiki-y-la-verificacion-de-las-demostraciones-matematicas\/","title":{"rendered":"ProofWiki y la verificaci\u00f3n de las demostraciones matem\u00e1ticas"},"content":{"rendered":"<p><a href=\"http:\/\/www.proofwiki.org\">ProofWiki<\/a> es un compendio de demostraciones matem\u00e1ticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matem\u00e1ticos.<\/p>\n<p>El proyecto empez\u00f3 en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en <a href=\"http:\/\/www.proofwiki.org\/wiki\/Category:Proofs\">34 categor\u00edas<\/a>. Una de las categor\u00edas particularmente interesante es la de <a href=\"http:\/\/www.proofwiki.org\/wiki\/Category:Named_Theorems\">teoremas con nombres<\/a> en la que aparecen 247 teoremas. Tambi\u00e9n es interesante la p\u00e1gina de los <a href=\"http:\/\/www.proofwiki.org\/wiki\/Special:PopularPages\">teoremas m\u00e1s populares<\/a> seg\u00fan el n\u00famero de visitas.<\/p>\n<p>ProofWiki podr\u00eda servir de base para otro proyecto cuyo objetivo final fuese la verificaci\u00f3n formal de las demostraciones matem\u00e1ticas. Para ello se podr\u00eda crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL\/Isar<\/a>, <a href=\"http:\/\/pvs.csl.sri.com\/\">PVS<\/a>, <a href=\"http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/\">ACL2<\/a>, <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a>, <a href=\"http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/\">HOL<\/a>, <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a> o <a href=\"http:\/\/mizar.org\/\">Mizar<\/a>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>ProofWiki es un compendio de demostraciones matem\u00e1ticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matem\u00e1ticos. El proyecto empez\u00f3 en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categor\u00edas. Una de las categor\u00edas particularmente interesante&#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":[8],"tags":[49,45,22,85,144,148,277,273,275],"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\/1133"}],"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=1133"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1133\/revisions"}],"predecessor-version":[{"id":2952,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1133\/revisions\/2952"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1133"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1133"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1133"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}