{"id":7223,"date":"2020-08-03T19:48:56","date_gmt":"2020-08-03T17:48:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7223"},"modified":"2020-08-28T19:51:52","modified_gmt":"2020-08-28T17:51:52","slug":"proyecto-formatus-formalizacion-de-las-matematicas-de-la-us","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proyecto-formatus-formalizacion-de-las-matematicas-de-la-us\/","title":{"rendered":"Proyecto ForMatUS (Formalizaci\u00f3n de las Matem\u00e1ticas de la US)"},"content":{"rendered":"<p>El proyecto <b>ForMatUS<\/b> tiene como objetivo la formalizaci\u00f3n de las matem\u00e1ticas ense\u00f1adas en la Universidad de Sevilla, fundamentalmente las asignaturas del <a href=\"https:\/\/bit.ly\/2YGNxGu\">Grado en Matem\u00e1ticas<\/a>.<\/p>\n<p>Los sistemas elegidos, inicialmente, para la formalizaci\u00f3n son <a href=\"https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> y <a href=\"https:\/\/leanprover.github.io\/about\/\">Lean<\/a>.<\/p>\n<p>El primero, Isabelle\/HOL, se ha usado en la asignatura de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf\/\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> (de 3\u00ba del Grado en Matem\u00e1ticas) y en la de <a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\/\">Razonamiento autom\u00e1tico<\/a> (del <a href=\"http:\/\/www.cs.us.es\/blogs\/mulcia\/docencia-plan-estudios\/\">M\u00e1ster Universitario en L\u00f3gica, Computaci\u00f3n e Inteligencia Artificial<\/a>). Adem\u00e1s, este curso los v\u00eddeos de las clases con Isabelle\/HOL se han subido a YouTube en la lista <a href=\"https:\/\/www.youtube.com\/playlist?list=PLPIlzBVlfbbFZOY6tpFiXMSw0j21OfHVY\">Razonamiento con Isabelle\/HOL<\/a> que puede servir como introducci\u00f3n al uso del sistema.<\/p>\n<p>El segundo, Lean, no se ha usado a\u00fan en ninguna de las asignaturas de la Universidad de Sevilla; pero s\u00ed he elaborado durante este curso algunos apuntes sobre el mismo:<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Logica_y_demostracion_con_Lean\/Indice.html\">L\u00f3gica y demostraci\u00f3n con Lean<\/a> es un resumen del curso <a href=\"http:\/\/leanprover.github.io\/logic_and_proof\/\">Logic and proof<\/a> (de Jeremy Avigad, Robert Y. Lewis y Floris van Doorn).<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/DN_en_Lean\/Indice.html\">Deducci\u00f3n natural en Lean<\/a> es una presentaci\u00f3n de las reglas de deducci\u00f3n natural en Lean mediante ejemplos b\u00e1sicos.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Tacticas_basicas_de_Lean\/Indice.html\">T\u00e1cticas b\u00e1sicas de Lean<\/a> es un resumen de las t\u00e1cticas b\u00e1sicas de Lean, con ejemplos, basado en <a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/lean_together\/source\/tactics\/tacticindex.html#basic-tactic-list\">Basic guide to tactics<\/a> de Kevin Buzzard.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Tacticas_en_Lean\/Indice.html\">Demostraciones aplicativas en Lean<\/a> es una adaptaci\u00f3n del cap\u00edtulo 5 (<a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/tactics.html\">Tactics<\/a>) del libro <a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/\">Theorem proving in Lean<\/a> de Jeremy Avigad, Leonardo de Moura y Soonho Kong.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Interaccion_con_Lean\/Indice.html\">Interacci\u00f3n con Lean<\/a> es una adaptaci\u00f3n del cap\u00edtulo 6 (<a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/interacting_with_lean.html\">Interacting with Lean<\/a>) del libro <a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/\">Theorem proving in Lean<\/a> de Jeremy Avigad, Leonardo de Moura y Soonho Kong.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Tipos_inductivos_en_Lean\/Indice.html#orgec75fb0\">Tipos inductivos en Lean<\/a> es una adaptaci\u00f3n del cap\u00edtulo 7 (<a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/inductive_types.html\">Inductive types<\/a>) del libro <a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/\">Theorem proving in Lean<\/a> de Jeremy Avigad, Leonardo de Moura y Soonho Kong.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"file:\/\/\/home\/jalonso\/ownCloud\/public_html\/apuntes\/Induccion_y_recursion_en_Lean\/Indice.html\">Inducci\u00f3n y recursi\u00f3n en Lean<\/a> es una adaptaci\u00f3n del cap\u00edtulo 8 (<a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/induction_and_recursion.html\">Induction and recursion<\/a>) del libro <a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/\">Theorem proving in Lean<\/a> de Jeremy Avigad, Leonardo de Moura y Soonho Kong.<\/li>\n<\/ul>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Resumenes_de_Lean.html\">Res\u00famenes de Lean<\/a> es una recopilaci\u00f3n de enlaces con res\u00famenes sobre sintaxis y t\u00e1cticas de Lean<\/li>\n<\/ul>\n<p>El desarrollo del proyecto lo ir\u00e9 anunciando en Twitter con la etiqueta <a href=\"https:\/\/twitter.com\/search?q=%23ForMatUS%20from%3AJose_A_Alonso&amp;src=typed_query&amp;f=live\">#ForMatUS<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El proyecto ForMatUS tiene como objetivo la formalizaci\u00f3n de las matem\u00e1ticas ense\u00f1adas en la Universidad de Sevilla, fundamentalmente las asignaturas del Grado en Matem\u00e1ticas. Los sistemas elegidos, inicialmente, para la formalizaci\u00f3n son Isabelle\/HOL y Lean. El primero, Isabelle\/HOL, se ha usado en la asignatura de L\u00f3gica matem\u00e1tica y fundamentos (de 3\u00ba del Grado en Matem\u00e1ticas)&#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":[335],"tags":[166,144,336],"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\/7223"}],"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=7223"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7223\/revisions"}],"predecessor-version":[{"id":7224,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7223\/revisions\/7224"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7223"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7223"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7223"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}