{"id":3407,"date":"2013-06-18T06:21:21","date_gmt":"2013-06-18T06:21:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3407"},"modified":"2013-06-18T06:21:21","modified_gmt":"2013-06-18T06:21:21","slug":"resena-formal-mathematics-on-display-a-wiki-for-flyspeck","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-mathematics-on-display-a-wiki-for-flyspeck\/","title":{"rendered":"Rese\u00f1a: Formal mathematics on display: A wiki for Flyspeck"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre la gesti\u00f3n del conocimiento matem\u00e1tico titulado <a href=\"http:\/\/bit.ly\/19LPT8g\">Formal mathematics on display: A wiki for Flyspeck<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.cs.ru.nl\/~carst\/\">Carst Tankink<\/a>, <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/cek\/\">Cezary Kaliszyk<\/a>, <a href=\"http:\/\/cs.ru.nl\/~urban\/\">Josef Urban<\/a> y <a href=\"http:\/\/cs.ru.nl\/~herman\/\">Herman Geuvers<\/a>.<\/p>\n<p>El trabajo se presentar\u00e1 en las <a href=\"http:\/\/www.cicm-conference.org\/2013\/cicm.php\">CICM 2013<\/a> (<i>Conferences on Intelligent Computer Mathematics<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe <a href=\"http:\/\/mws.cs.ru.nl\/agora_cicm\/flyspeck\/Home\/\">Agora system<\/a> is a prototype &#8220;Wiki for Formal Mathematics&#8221;, with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI\/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype <a href=\"http:\/\/mws.cs.ru.nl\/agora_cicm\/flyspeck\/\">Flyspeck Wiki<\/a> as an instance of Agora for <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/\">HOL Light<\/a> formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales&#8217;s informal Flyspeck book, and the formal Flyspeck development.<\/p>\n<p>The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre la gesti\u00f3n del conocimiento matem\u00e1tico titulado Formal mathematics on display: A wiki for Flyspeck. Sus autores son Carst Tankink, Cezary Kaliszyk, Josef Urban y Herman Geuvers. El trabajo se presentar\u00e1 en las CICM 2013 (Conferences on Intelligent Computer Mathematics). Su resumen es The Agora system is a prototype &#8220;Wiki&#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":[22,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\/3407"}],"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=3407"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3407\/revisions"}],"predecessor-version":[{"id":3408,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3407\/revisions\/3408"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3407"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3407"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3407"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}