{"id":7625,"date":"2021-12-26T12:39:57","date_gmt":"2021-12-26T11:39:57","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7625"},"modified":"2021-12-26T13:25:16","modified_gmt":"2021-12-26T12:25:16","slug":"resena-why-formalize-mathematics","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-why-formalize-mathematics\/","title":{"rendered":"Rese\u00f1a: Why formalize mathematics?"},"content":{"rendered":"<div id=\"content\">\n<p>Se ha publicado un art\u00edculo sobre razonamiento formalizado titulado <a href=\"https:\/\/www.imo.universite-paris-saclay.fr\/~pmassot\/files\/exposition\/why_formalize.pdf\">Why formalize mathematics?<\/a><\/p>\n<p>Su autor es <a href=\"https:\/\/www.imo.universite-paris-saclay.fr\/~pmassot\/en\/\">Patrick Massot<\/a> (del <a href=\"http:\/\/www.math.u-psud.fr\/\">Laboratoire de math\u00e9matiques d\u2019Orsay<\/a> en la <a href=\"http:\/\/www.u-psud.fr\/\">Universit\u00e9 Paris-Saclay<\/a>, Orsay, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>We\u2019ve been doing mathematics for more than two thousand years with remarkable success. Hence it is natural to be puzzled by people investing a lot of time and energy into a very new and weird way of doing mathematics: the formalized way where human beings explain mathematical definitions and proofs to computers. Beyond puzzlement, some people are wary. They think the traditional way may disappear, or maybe even mathematicians may disappear, being replaced by AI agents. These events are extremely unlikely and they are not the goals of the mathematical formalization community. We want to add to our tool set, without losing anything we already have. In this text I\u2019ll explain what we want to add, distinguishing what already partially exists and what is currently science fiction. Examples will use Lean, a proof assistant software developed mostly by Leonardo de Moura at Microsoft Research, but everything I\u2019ll write applies to other proof assistants such as Coq or Isabelle.<\/p><\/blockquote>\n<p>El trabajo es una ampliaci\u00f3n de la charla con el mismo t\u00edtulo impartida el 27 de octubre de 2021 en el seminario <a href=\"https:\/\/cmsa.fas.harvard.edu\/tech-in-math\/\">New Technologies in Mathematics Seminar Series<\/a> en Harvard. El v\u00eddeo de la charla se encuentra en este <a href=\"https:\/\/youtu.be\/rRGh97sOtKE\">enlace<\/a>.<\/p>\n<p>Finalmente, a continuaci\u00f3n se muestra un resumen m\u00e1s detallado de su contenido.<\/p>\n<div id=\"table-of-contents\">\n<h2>\u00cdndice<\/h2>\n<div id=\"text-table-of-contents\">\n<ul>\n<li><a href=\"#org108d7bd\">1. Verificar demostraciones<\/a><\/li>\n<li><a href=\"#orga61bb2e\">2. Explicar y aprender<\/a><\/li>\n<li><a href=\"#org6260d71\">3. Ense\u00f1ar<\/a><\/li>\n<li><a href=\"#orgd999b53\">4. Crear nuevas matem\u00e1ticas<\/a><\/li>\n<li><a href=\"#org767f824\">5. Colaborar y divertirse<\/a><\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org108d7bd\" class=\"outline-2\">\n<h2 id=\"org108d7bd\"><span class=\"section-number-2\">1.<\/span> Verificar demostraciones<\/h2>\n<div id=\"text-1\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>La ventaja m\u00e1s evidente de las matem\u00e1ticas formalizadas es la certeza de que una prueba es correcta cuando ha sido comprobada por un ordenador.<\/li>\n<li>La verificaci\u00f3n por el ordenador garantiza la integridad y la consistencia a todas las escalas.\n<ul class=\"org-ul\">\n<li>La consistencia a peque\u00f1a escala significa que no hay ning\u00fan caso l\u00edmite olvidado (como el conjunto vac\u00edo o el \u00fanico n\u00famero primo par).<\/li>\n<li>La exhaustividad consiste en asegurarse de que no hay afirmaciones impl\u00edcitas err\u00f3neas.<\/li>\n<li>La consistencia a mediana escala significa que no dejan de ser correctos los lemas cuando modificamos definiciones.<\/li>\n<li>La consistencia a gran escala significa que no permitimos que se produzcan malentendidos al utilizar un teorema de un documento que ten\u00eda una suposici\u00f3n o notaci\u00f3n ligeramente diferente.<\/li>\n<\/ul>\n<\/li>\n<li>La tecnolog\u00eda actual no permite esperar que pronto tengamos pruebas formales de cualquier art\u00edculo publicado porque:\n<ul class=\"org-ul\">\n<li>La formalizaci\u00f3n lleva demasiado tiempo por ahora.<\/li>\n<li>No tenemos suficiente matem\u00e1tica formalizada sobre la que basarnos.<\/li>\n<\/ul>\n<\/li>\n<li>Alternativas posibles:\n<ul class=\"org-ul\">\n<li>Podemos concentrarnos en partes de teoremas grandes, como en el <a href=\"https:\/\/xenaproject.wordpress.com\/2020\/12\/05\/liquid-tensor-experiment\/\">Liquid tensor experiment<\/a>.<\/li>\n<li>Verificaci\u00f3n de pruebas demasiados grandes para el cerebro humano, como en el teorema de los cuatros colores o en la conjetura de Kepler.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orga61bb2e\" class=\"outline-2\">\n<h2 id=\"orga61bb2e\"><span class=\"section-number-2\">2.<\/span> Explicar y aprender<\/h2>\n<div id=\"text-2\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>Al escribir textos matem\u00e1ticos hay que elegir los conocimientos previos asumidos y seleccionar un nivel de detalle.<\/li>\n<li>La aplicaci\u00f3n m\u00e1s prometedora de las matem\u00e1ticas formalizadas es el sue\u00f1o de producir documentos matem\u00e1ticos que permitan a los lectores elegir din\u00e1micamente el nivel de detalle y el conocimiento usado.<\/li>\n<li>Una vez que se entiende una afirmaci\u00f3n, se puede pasar a su demostraci\u00f3n.\n<ul class=\"org-ul\">\n<li>La capacidad inform\u00e1tica m\u00e1s importante es la visualizaci\u00f3n del &#8220;estado t\u00e1ctico&#8221;, que es una lista de todos los objetos y supuestos que son relevantes en ese momento y el objetivo actual de la prueba.<\/li>\n<li>Esta informaci\u00f3n cambia en cada paso de la prueba.<\/li>\n<\/ul>\n<\/li>\n<li>La idea es tener un documento progresivo en el que los lectores puedan elegir din\u00e1micamente d\u00f3nde pedir los detalles cuando los necesiten.<\/li>\n<li>Actualmente no tenemos una forma muy agradable de presentar esta informaci\u00f3n, pero esperamos tenerla en un par de a\u00f1os como m\u00e1ximo.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org6260d71\" class=\"outline-2\">\n<h2 id=\"org6260d71\"><span class=\"section-number-2\">3.<\/span> Ense\u00f1ar<\/h2>\n<div id=\"text-3\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>Hay que ense\u00f1ar a concebir y escribir pruebas.<\/li>\n<li>Muy a menudo, esto se ense\u00f1a s\u00f3lo indirectamente: se pretende que los alumnos aprendan por imitaci\u00f3n.<\/li>\n<li>Ense\u00f1ar utilizando un asistente de pruebas tiene el coste obvio de poner una barrera tecnol\u00f3gica a la entrada (aprender sintaxis y navegar por el software). Pero tambi\u00e9n tiene grandes ventajas.\n<ul class=\"org-ul\">\n<li>Una ventaja es el estado t\u00e1ctico que se muestra de forma interactiva durante la escritura de pruebas.<\/li>\n<li>La obligaci\u00f3n establecer formalmente el enunciado y separarlo de la demostraci\u00f3n.<\/li>\n<\/ul>\n<\/li>\n<li>Ejemplo de demostraci\u00f3n en Lean literario:\n<pre class=\"example\">example (f : \u211d \u2192 \u211d) (u : \u2115 \u2192 \u211d) (x\u2080 : \u211d)\n  (hu : sequence_tendsto u x\u2080) (hf : continuous_function_at f x\u2080) :\nsequence_tendsto (f \u2218 u) (f x\u2080) :=\nbegin\n  Let's prove that \u2200 \u03b5 &gt; 0, \u2203 N, \u2200 n \u2265 N, |f (u n) - f x\u2080| \u2264 \u03b5,\n  Fix \u03b5 &gt; 0,\n  By hf applied to \u03b5 using \u03b5_pos we obtain \u03b4 such that\n    (\u03b4_pos : \u03b4 &gt; 0) (Hf : \u2200 (x : \u211d), |x - x\u2080| \u2264 \u03b4 \u2192 |f x - f x\u2080| \u2264 \u03b5),\n  By hu applied to \u03b4 using \u03b4_pos we obtain N such that\n    Hu : \u2200 n \u2265 N, |u n - x\u2080| \u2264 \u03b4,\n  Let's prove that N works : \u2200 n \u2265 N, |f (u n) - f x\u2080| \u2264 \u03b5,\n  Fix n \u2265 N,\n  By Hf applied to u n it suffices to prove |u n - x\u2080| \u2264 \u03b4,\n  This is Hu applied to n using n_ge\nend\n<\/pre>\n<\/li>\n<li>Otra ventaja del uso de los asistentes de pruebas es que los alumnos pueden percibir mucho mejor la alternancia entre las fases en las que la estructura del objetivo dicta el siguiente movimiento y las fases en las que se requiere cierta iniciativa.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd999b53\" class=\"outline-2\">\n<h2 id=\"orgd999b53\"><span class=\"section-number-2\">4.<\/span> Crear nuevas matem\u00e1ticas<\/h2>\n<div id=\"text-4\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>El ordenador puede\n<ul class=\"org-ul\">\n<li>Volver a comprobar continuamente todo en cada cambio de definici\u00f3n o enunciado de lema, marcando (casi) instant\u00e1neamente lo que hay que modificar.<\/li>\n<li>Ayudar a la limpieza, por ejemplo, marcando los supuestos no utilizados.<\/li>\n<li>Aclarar qu\u00e9 lemas dependen de otros lemas y definiciones.<\/li>\n<li>Demostrar autom\u00e1ticamente pruebas pasos rutinarios o al menos sugerir un paso siguiente.<\/li>\n<\/ul>\n<\/li>\n<li>Formalizar mientras se crea es actualmente una enorme ralentizaci\u00f3n, incluso para los usuarios experimentados. La esperanza es que la tecnolog\u00eda mejore para que la formalizaci\u00f3n consuma mucho menos tiempo. Aqu\u00ed puede ayudar alguna forma de inteligencia artificial.<\/li>\n<li>Otro sue\u00f1o que necesita de la IA es un buen motor de b\u00fasqueda de enunciados matem\u00e1ticos.<\/li>\n<li>La principal ayuda a la creaci\u00f3n puede ser m\u00e1s indirecta. Las matem\u00e1ticas formalizadas requieren un <i>pensamiento claro<\/i>.<\/li>\n<li>Las matem\u00e1ticas formalizadas fomentan, o incluso a veces exigen, <i>abstracciones poderosas<\/i>.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org767f824\" class=\"outline-2\">\n<h2 id=\"org767f824\"><span class=\"section-number-2\">5.<\/span> Colaborar y divertirse<\/h2>\n<div id=\"text-5\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>Las matem\u00e1ticas formalizadas aportan mucha diversi\u00f3n. Parte de esta diversi\u00f3n proviene del aspecto de &#8220;videojuego&#8221; de los asistentes de pruebas. Pero la verdadera diversi\u00f3n proviene de la colaboraci\u00f3n.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"postamble\" class=\"status\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre razonamiento formalizado titulado Why formalize mathematics? Su autor es Patrick Massot (del Laboratoire de math\u00e9matiques d\u2019Orsay en la Universit\u00e9 Paris-Saclay, Orsay, Francia). Su resumen es We\u2019ve been doing mathematics for more than two thousand years with remarkable success. Hence it is natural to be puzzled by people investing a&#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":[100,1],"tags":[166],"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\/7625"}],"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=7625"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7625\/revisions"}],"predecessor-version":[{"id":7629,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7625\/revisions\/7629"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7625"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7625"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7625"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}