{"id":7618,"date":"2021-12-25T17:32:22","date_gmt":"2021-12-25T16:32:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7618"},"modified":"2021-12-26T11:54:57","modified_gmt":"2021-12-26T10:54:57","slug":"resena-what-is-the-point-of-computers-a-question-for-pure-mathematicians","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematicians\/","title":{"rendered":"Rese\u00f1a: What is the point of computers? A question for pure mathematicians"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobe razonamiento formalizado titulado <a href=\"https:\/\/www.ma.imperial.ac.uk\/~buzzard\/xena\/pdfs\/ICMtalkv0.pdf\">What is the point of computers? A question for pure mathematicians<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.imperial.ac.uk\/people\/k.buzzard\">Kevin Buzzard<\/a> (Imperial College in London, U.K.).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>We discuss the idea that computers might soon help pure mathematicians to prove theorems in areas where they have not previously been useful.<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en julio de 2022 como una conferencia invitada en el <a href=\"https:\/\/icm2022.org\/index\">ICM 2022<\/a>.<\/p>\n<p>Finalmente, 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=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org9884d17\">1. Introducci\u00f3n<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org5d76d56\">2. Breve historia de los teoremas verificados formalmente<\/a>\n<ul>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgd6b2542\">2.1. El siglo XX<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org691de33\">2.2. El teorema de los cuatro colores<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org78ca848\">2.3. El teorema de los n\u00fameros primos<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org3f3950f\">2.4. Teorema del orden impar<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org316c95c\">2.5. La conjetura de Kepler<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgd5a9708\">2.6. Espacios perfectoides<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgfce4451\">2.7. Matem\u00e1ticas condensadas<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org216fd64\">2.8. Otros resultados<\/a><\/li>\n<\/ul>\n<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org78f9f83\">3. mathlib<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org37fc150\">4. Una breve gu\u00eda de la teor\u00eda de tipos<\/a>\n<ul>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgb7abc4e\">4.1. \u00bfQu\u00e9 es un tipo?<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgd3773be\">4.2. Tipos inductivos<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgecac7fc\">4.3. Las proposiciones son tipos<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgd15809a\">4.4. Las pruebas son funciones<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org421207e\">4.5. Un ejemplo<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org7f77a7e\">4.6. Fundamentos<\/a><\/li>\n<\/ul>\n<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgc18d4f9\">5. El futuro<\/a>\n<ul>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgd38fd80\">5.1. Un nuevo tipo de documento matem\u00e1tico<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org9917f47\">5.2. B\u00fasqueda sem\u00e1ntica en una base de datos matem\u00e1tica<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#org6ffdb23\">5.3. Comprobaci\u00f3n de pruebas<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgf62f921\">5.4. La ense\u00f1anza<\/a><\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-what-is-the-point-of-computers-a-question-for-pure-mathematician#orgfb21f71\">5.5. Otras ideas<\/a><\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9884d17\" class=\"outline-2\">\n<h2 id=\"org9884d17\"><span class=\"section-number-2\">1.<\/span> Introducci\u00f3n<\/h2>\n<div id=\"text-1\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>Los ordenadores se han utilizado para ayudar a algunos matem\u00e1ticos puros a hacer su trabajo desde que existen los ordenadores.<\/li>\n<li>Birch y Swinnerton-Dyer utilizaron un ordenador para calcular muchos ejemplos de soluciones de ecuaciones c\u00fabicas en dos variables m\u00f3dulo n\u00fameros primos.<\/li>\n<li>Este art\u00edculo es un intento de explicar a todos los investigadores en matem\u00e1ticas puras que los ordenadores pueden utilizarse ahora para ayudarnos no s\u00f3lo a calcular, sino a razonar.<\/li>\n<li>Se trata de la posibilidad de que los ordenadores pronto nos ayuden a demostrar teoremas.<\/li>\n<li>No se debe esperar en los pr\u00f3ximos 10 a\u00f1os que un ordenador, por s\u00ed solo, consiga una demostraci\u00f3n de cualquier problema abierto de inter\u00e9s para los matem\u00e1ticos puros.<\/li>\n<li>Lo que se debe esperar en los pr\u00f3ximos 10 a\u00f1os:\n<ul class=\"org-ul\">\n<li>Que los ordenadores ayuden a los matem\u00e1ticos puros a demostrar teoremas.<\/li>\n<li>Bases de datos de matem\u00e1ticas digitalizadas y con capacidad de b\u00fasqueda sem\u00e1ntica.<\/li>\n<li>Que los ordenadores completen las pruebas de los lemas, se\u00f1alen contraejemplos a nuestras conjeturas y sugieran resultados que nos podr\u00edan ser \u00fatiles.<\/li>\n<\/ul>\n<\/li>\n<li>La formalizaci\u00f3n es la matem\u00e1tica reinterpretada como un juego de ordenador.<\/li>\n<li>Los primeros asistentes de pruebas por ordenador aparecieron en los a\u00f1os sesenta.<\/li>\n<li>M\u00e1s recientemente han ocurrido dos cosas:\n<ul class=\"org-ul\">\n<li>Los resultados a nivel de investigaci\u00f3n en todas las \u00e1reas tradicionales de las matem\u00e1ticas puras son ahora accesibles a estos sistemas.<\/li>\n<li>Muchos asistentes de pruebas modernos admiten &#8220;t\u00e1cticas&#8221;, lo que permite a los matem\u00e1ticos comunicarse con estas m\u00e1quinas de un modo de alto nivel, similar al modo en que se comunican entre s\u00ed.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org5d76d56\" class=\"outline-2\">\n<h2 id=\"org5d76d56\"><span class=\"section-number-2\">2.<\/span> Breve historia de los teoremas verificados formalmente<\/h2>\n<div id=\"text-2\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>M\u00e1s informaci\u00f3n en el art\u00edculo <a href=\"https:\/\/arxiv.org\/abs\/1302.2898\">Mathematics in the Age of the Turing Machine<\/a> de Thomas Hales.<\/li>\n<\/ul>\n<\/div>\n<div id=\"outline-container-orgd6b2542\" class=\"outline-3\">\n<h3 id=\"orgd6b2542\"><span class=\"section-number-3\">2.1.<\/span> El siglo XX<\/h3>\n<div id=\"text-2-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Pruebas de\n<ul class=\"org-ul\">\n<li>La ra\u00edz cuadrada de 2 es irracional.<\/li>\n<li>Hay infinitos n\u00fameros primos.<\/li>\n<li>Si x e y son n\u00fameros reales, entonces (x + y)(x + 2y)(x + 3y) = x\u00b3 + 6x\u00b2y + 11xy\u00b2 + 6y\u00b3 se puede demostrar con la t\u00e1ctica <code>ring<\/code>.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org691de33\" class=\"outline-3\">\n<h3 id=\"org691de33\"><span class=\"section-number-3\">2.2.<\/span> El teorema de los cuatro colores<\/h3>\n<div id=\"text-2-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Una de sus formulaciones es la afirmaci\u00f3n de que los v\u00e9rtices de todo grafo plano (sin bucles) pueden colorearse con cuatro colores de forma que ning\u00fan v\u00e9rtice adyacente comparta un color.<\/li>\n<li>En 1976, Appel y Haken lo probaron utilizando un ordenador de manera esencial.\n<ul class=\"org-ul\">\n<li>En este caso el ordenador se utilizaba para calcular y no para demostrar.<\/li>\n<li>La prueba se basa, esencialmente, en un c\u00e1lculo inform\u00e1tico y, por tanto, depende de la correcci\u00f3n del c\u00f3digo inform\u00e1tico.<\/li>\n<\/ul>\n<\/li>\n<li>En 2005, Georges Gonthier verific\u00f3 formalmente el resultado de Appel-Haken .\n<ul class=\"org-ul\">\n<li>El trabajo consta de 60.000 l\u00edneas de c\u00f3digo escritas en el asistente de pruebas Coq.<\/li>\n<li>Comprende pruebas en topolog\u00eda y teor\u00eda de grafos, al tiempo que verifica formalmente el c\u00e1lculo inform\u00e1tico necesario para terminar la prueba.<\/li>\n<li>Gran parte del trabajo consisti\u00f3 en escribir material de base en lugar de formalizar la prueba en s\u00ed.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org78ca848\" class=\"outline-3\">\n<h3 id=\"org78ca848\"><span class=\"section-number-3\">2.3.<\/span> El teorema de los n\u00fameros primos<\/h3>\n<div id=\"text-2-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>En 2007, un equipo formado por Jeremy Avigad, Kevin Donnelly, David Gray y Paul Raff verific\u00f3 formalmente el teorema de los n\u00fameros primos, en el sistema Isabelle\/HOL.\n<ul class=\"org-ul\">\n<li>El trabajo se basaba en las teor\u00edas de la aritm\u00e9tica y el an\u00e1lisis real b\u00e1sico.<\/li>\n<li>En 2007, las matem\u00e1ticas m\u00e1s serias de nivel de licenciatura y de m\u00e1ster ya eran, en teor\u00eda, accesibles a estos sistemas, al menos en algunas \u00e1reas de las matem\u00e1ticas puras.<\/li>\n<\/ul>\n<\/li>\n<li>En 2009, John Harrison formaliz\u00f3 la prueba anal\u00edtica compleja del teorema de los n\u00fameros primos en HOL Light.<\/li>\n<li>En 2016, Mario Carneiro formaliz\u00f3 la prueba en Metamath.<\/li>\n<li>Una de las razones por las que el resultado se estaba formalizando de forma independiente en varios demostradores de teoremas era que resultaba extremadamente dif\u00edcil traducir una demostraci\u00f3n escrita en uno de los sistemas a una demostraci\u00f3n en otro sistema.<\/li>\n<li>En 2020, Mario Carneiro tradujo la prueba a Lean.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org3f3950f\" class=\"outline-3\">\n<h3 id=\"org3f3950f\"><span class=\"section-number-3\">2.4.<\/span> Teorema del orden impar<\/h3>\n<div id=\"text-2-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>El teorema del orden impar afirma que cualquier grupo finito de orden impar es resoluble.<\/li>\n<li>En 2013, un equipo de 15 personas dirigido por Gonthier verific\u00f3 formalmente una prueba de este teorema en Coq.<\/li>\n<li>La prueba es muy larga; un argumento completo (modulo los fundamentos en teor\u00eda de grupos y representaciones) se presenta en los dos vol\u00famenes.<\/li>\n<li>El teorema est\u00e1 mucho m\u00e1s all\u00e1 de las matem\u00e1ticas de nivel de maestr\u00eda (este trabajo fue una de las razones por las que Thompson fue galardonado con la Medalla Fields en 1970).<\/li>\n<li>La prueba de Coq implic\u00f3 la formalizaci\u00f3n de los dos libros mencionados anteriormente, adem\u00e1s de la teor\u00eda de grupos, la teor\u00eda de la representaci\u00f3n, la teor\u00eda de Galois y la teor\u00eda de los n\u00fameros.<\/li>\n<li>La formalizaci\u00f3n del material de base ocup\u00f3 gran parte de los seis a\u00f1os que los autores dedicaron a la prueba.<\/li>\n<li>Lo que este trabajo de formalizaci\u00f3n nos muestra es que los demostradores de teoremas son ahora capaces de operar a este tipo de escala.<\/li>\n<li>Por t\u00e9rmino medio, una l\u00ednea de matem\u00e1ticas en los libros de texto correspond\u00eda a cinco l\u00edneas de c\u00f3digo inform\u00e1tico, por lo que sabemos que en 2013 el llamado &#8220;factor De Bruijn&#8221; para este tipo de matem\u00e1ticas es de alrededor de 5.<\/li>\n<li>Los grandes proyectos de formalizaci\u00f3n como \u00e9ste son una forma muy eficaz de motivar el desarrollo de bibliotecas de matem\u00e1ticas fundamentales.<\/li>\n<li>Una de las consecuencias de este proyecto de formalizaci\u00f3n fue que Coq desarroll\u00f3 una biblioteca muy s\u00f3lida de \u00e1lgebra de nivel universitario que, por supuesto, puede utilizarse (y se utiliza) para otros proyectos.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org316c95c\" class=\"outline-3\">\n<h3 id=\"org316c95c\"><span class=\"section-number-3\">2.5.<\/span> La conjetura de Kepler<\/h3>\n<div id=\"text-2-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>La conjetura de Kepler afirma que el empaquetamiento c\u00fabico centrado en la cara es la forma m\u00e1s densa de empaquetar esferas congruentes en el espacio.<\/li>\n<li>En 1998, Hales y Ferguson demostraron la conjetura.\n<ul class=\"org-ul\">\n<li>Parte de la prueba de Hales-Ferguson consisti\u00f3 en la comprobaci\u00f3n de m\u00e1s de 23.000 desigualdades no lineales en un ordenador.<\/li>\n<li>Tambi\u00e9n se realizaron otros c\u00e1lculos inform\u00e1ticos.<\/li>\n<\/ul>\n<\/li>\n<li>En 2003 Hales anunci\u00f3 un proyecto para verificar formalmente la prueba.\n<ul class=\"org-ul\">\n<li>El proyecto de formalizaci\u00f3n tard\u00f3 unos 12 a\u00f1os en completarse, y comprendi\u00f3 m\u00e1s de medio mill\u00f3n de l\u00edneas de c\u00f3digo.<\/li>\n<li>Uno de los principales beneficios del trabajo es que la biblioteca est\u00e1ndar de HOL Light creci\u00f3 hasta incluir teoremas como el teorema del punto fijo de Brouwer, el teorema de Krein-Milman y el teorema de Stone- Weierstrass.<\/li>\n<\/ul>\n<\/li>\n<li>En 2017, Hales dio una charla en la que cuenta la historia de la prueba de Kepler y explica su visi\u00f3n para el futuro de las matem\u00e1ticas formalizadas.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd5a9708\" class=\"outline-3\">\n<h3 id=\"orgd5a9708\"><span class=\"section-number-3\">2.6.<\/span> Espacios perfectoides<\/h3>\n<div id=\"text-2-6\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Este proyecto implicaba el desarrollo de teor\u00edas b\u00e1sicas de localizaci\u00f3n de anillos y de gavillas en espacios topol\u00f3gicos.<\/li>\n<li>El proyecto aclar\u00f3 que deber\u00eda ser posible formalizar objetos matem\u00e1ticos mucho m\u00e1s complejos.<\/li>\n<li>A finales de 2017 a Patrick Massot y a Kevin Buzzard se les ocurri\u00f3 de forma independiente la idea de formalizar los espacios perfectoides. En 2018 Johan Commelin se uni\u00f3 al proyecto.<\/li>\n<li>El proyecto se podr\u00eda resumir como una formalizaci\u00f3n inform\u00e1tica de la \u00fanica l\u00ednea matem\u00e1tica &#8220;sea X un espacio perfectoide&#8221;<\/li>\n<li>La principal ganancia fue la ampliaci\u00f3n de la biblioteca matem\u00e1tica de Lean, mathlib, con los resultados de la Topolog\u00eda General de Bourbaki as\u00ed como muchos resultados del \u00e1lgebra topol\u00f3gica y los inicios de una teor\u00eda de campos de valoraci\u00f3n discretos.<\/li>\n<li>La siguiente pregunta natural es si los sistemas de demostraci\u00f3n por ordenador pueden demostrar teoremas complejos sobre objetos complejos.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgfce4451\" class=\"outline-3\">\n<h3 id=\"orgfce4451\"><span class=\"section-number-3\">2.7.<\/span> Matem\u00e1ticas condensadas<\/h3>\n<div id=\"text-2-7\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Clausen y Scholze han estado desarrollando una teor\u00eda de las matem\u00e1ticas condensadas, con el objetivo de conseguir que las t\u00e9cnicas del \u00e1lgebra homol\u00f3gica se apliquen a varios problemas de la teor\u00eda de la geometr\u00eda anal\u00edtica.<\/li>\n<li>Scholze desafi\u00f3 a la comunidad de la formalizaci\u00f3n para demostrar su Teorema 9.1 en una entrada de su blog.<\/li>\n<li>Johan Commelin se convirti\u00f3 en el l\u00edder de facto del proceso de formalizaci\u00f3n, y Patrick Massot le apoy\u00f3 y un equipo de te\u00f3ricos de n\u00fameros algebraicos y ge\u00f3metras aritm\u00e9ticos comenz\u00f3 a trabajar en el proyecto.<\/li>\n<li>En seis meses, el equipo hab\u00eda crecido hasta contar con m\u00e1s de diez personas y hab\u00eda formalizado una demostraci\u00f3n completa del teorema 9.4.<\/li>\n<li>En el momento de escribir estas l\u00edneas no se ha deemostrado el teorema 9.1, pero es s\u00f3lo cuesti\u00f3n de tiempo.<\/li>\n<li>Esto representa una prueba sustancial de que ahora cualquier matem\u00e1tica pura puede formalizarse con demostradores de teoremas.<\/li>\n<li>En muchos proyectos de formalizaci\u00f3n se suele dedicar una \u0001cantidad de tiempo considerable a la formalizaci\u00f3n del material de base.<\/li>\n<li>A medida que las bibliotecas de los demostradores mejoren y empiecen a contener el tipo de material que los matem\u00e1ticos en activo dan por sentado, habr\u00e1 menos de estos &#8220;costes iniciales&#8221;.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org216fd64\" class=\"outline-3\">\n<h3 id=\"org216fd64\"><span class=\"section-number-3\">2.8.<\/span> Otros resultados<\/h3>\n<div id=\"text-2-8\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Sebastien Gou\u00ebzel formaliz\u00f3 las definiciones b\u00e1sicas de los \u221ecolectores C<sup>k<\/sup> y C en Lean.<\/li>\n<li>Mahboubi y Sibut-Pinote demostraron la irracionalidad de \u03b6(3) en Coq y Eberl lo demostr\u00f3 en Isabelle\/HOL.<\/li>\n<li>Han y van Doorn demostraron la independencia de la hip\u00f3tesis del continuo en Lean.<\/li>\n<li>Immler verific\u00f3 formalmente los c\u00e1lculos de Tucker utilizados para verificar la existencia del atractor extra\u00f1o.<\/li>\n<li>Mehta y Dillies verificaron formalmente el teorema de Roth sobre las progresiones aritm\u00e9ticas en Lean.<\/li>\n<li>Argyraki, Edmonds y Paulson verificaron el teorema de Szemeredi en Isabelle\/HOL.<\/li>\n<li>La resoluci\u00f3n de Ellenberg-Gijswijt de la conjetura del conjunto tope fue verificada en Lean por Dahmen, H\u00f6lzl y Lewis.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org78f9f83\" class=\"outline-2\">\n<h2 id=\"org78f9f83\"><span class=\"section-number-2\">3.<\/span> mathlib<\/h2>\n<div id=\"text-3\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>mathlib:\n<ul class=\"org-ul\">\n<li>Es la biblioteca de matem\u00e1ticas de Lean.<\/li>\n<li>Es una de las mayores colecciones de matem\u00e1ticas formalizadas que existen.<\/li>\n<li>Actualmente est\u00e1 experimentando un r\u00e1pido crecimiento.<\/li>\n<\/ul>\n<\/li>\n<li>En 2013, Leonardo de Moura inici\u00f3 el desarrollo del Lean Theorem Prover.<\/li>\n<li>En 2017, se decidi\u00f3 separar la mayor parte de la parte &#8220;matem\u00e1tica&#8221; del prover de la parte &#8220;central&#8221;, y trasladar las matem\u00e1ticas a una biblioteca propia. De esta forma naci\u00f3 mathlib.<\/li>\n<li>En el 2017, mathlib conten\u00eda definiciones de grupos, anillos y topolog\u00eda espacios, filtros, una construcci\u00f3n de los n\u00fameros racionales (los naturales y los enteros se quedaron en el n\u00facleo de Lean), y poco m\u00e1s.<\/li>\n<li>Johannes H\u00f6lzl y Mario Carneiro se convirtieron en los mantenedores de mathlib.<\/li>\n<li>La biblioteca es un proyecto gratuito y de c\u00f3digo abierto.<\/li>\n<li>mathlib tiene ahora m\u00e1s de 200 colaboradores.<\/li>\n<li>Uno de los principios de la biblioteca es hacer las cosas &#8220;en la generalidad correcta&#8221;.<\/li>\n<li>La biblioteca no est\u00e1 concebida con fines pedag\u00f3gicos o de legibilidad; la idea es seguir creando una base s\u00f3lida para el tipo de matem\u00e1ticas que se dan en un departamento de matem\u00e1ticas puras contempor\u00e1neo.<\/li>\n<li>Es interesante observar que Lean parece estar aprendiendo matem\u00e1ticas m\u00e1s o menos a la misma velocidad que un estudiante universitario.<\/li>\n<li>Para tener una idea actualizada del estado actual de mathlib, lo mejor es echar un vistazo a la descripci\u00f3n completa de mathlib de la comunidad Lean <a href=\"https:\/\/leanprover-community.github.io\/mathlib-overview.html\">aqu\u00ed<\/a>, o a su resumen de las matem\u00e1ticas de nivel universitario que contiene <a href=\"https:\/\/leanprover-community.github.io\/undergrad.html\">aqu\u00ed<\/a>.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org37fc150\" class=\"outline-2\">\n<h2 id=\"org37fc150\"><span class=\"section-number-2\">4.<\/span> Una breve gu\u00eda de la teor\u00eda de tipos<\/h2>\n<div id=\"text-4\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li>Muchos demostradores de teoremas modernos utilizan alguna versi\u00f3n de la teor\u00eda de tipos como base.\n<ul class=\"org-ul\">\n<li>Isabelle\/HOL y los otros sistemas HOL utilizan la teor\u00eda de tipos simple.<\/li>\n<li>Lean y Coq utilizan la teor\u00eda de tipos dependiente.<\/li>\n<li>Los diversos sistemas HoTT utilizan la teor\u00eda de tipos de homotop\u00eda.<\/li>\n<\/ul>\n<\/li>\n<li>Hoy en d\u00eda la mayor\u00eda de las matem\u00e1ticas que se realizan en los demostradores de teoremas se hacen en un sistema de teor\u00eda de tipos,<\/li>\n<\/ul>\n<\/div>\n<div id=\"outline-container-orgb7abc4e\" class=\"outline-3\">\n<h3 id=\"orgb7abc4e\"><span class=\"section-number-3\">4.1.<\/span> \u00bfQu\u00e9 es un tipo?<\/h3>\n<div id=\"text-4-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>En definiciones como la de grupo, la palabra &#8220;conjunto&#8221; no significa m\u00e1s que &#8220;colecci\u00f3n de elementos&#8221;.<\/li>\n<li>En la teor\u00eda de tipos, el papel de &#8220;colecci\u00f3n de elementos&#8221; lo desempe\u00f1a el tipo.<\/li>\n<li>Un tipo es una colecci\u00f3n de t\u00e9rminos.<\/li>\n<li>La definici\u00f3n de un grupo en la teor\u00eda de tipos: un grupo es un tipo dotado de multiplicaci\u00f3n tal que se cumplen algunos axiomas.<\/li>\n<li>La \u00fanica diferencia es la notaci\u00f3n: el `a \u2208 X` de la teor\u00eda de conjuntos se sustituye por el `a : X` de la teor\u00eda de tipos.<\/li>\n<li>En la teor\u00eda de tipos, todo es un t\u00e9rmino, y todo t\u00e9rmino tiene un tipo, pero no todo t\u00e9rmino es un tipo.<\/li>\n<li>Una diferencia entre los tipos y los conjuntos es que los tipos no se mezclan: los tipos distintos son disjuntos.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd3773be\" class=\"outline-3\">\n<h3 id=\"orgd3773be\"><span class=\"section-number-3\">4.2.<\/span> Tipos inductivos<\/h3>\n<div id=\"text-4-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>En Lean se pueden definir tipos &#8220;inductivamente&#8221;. Por ejemplo, la definici\u00f3n de los naturales es as\u00ed:\n<pre class=\"example\">nat inductive\n| cero : nat\n| suc (n : nat) : nat\n<\/pre>\n<p>Con la definici\u00f3n se obtienen:<\/p>\n<ul class=\"org-ul\">\n<li>constructores_\n<ul class=\"org-ul\">\n<li><code>nat.cero ; nat<\/code><\/li>\n<li><code>nat.suc : nat -&gt; nat<\/code><\/li>\n<\/ul>\n<\/li>\n<li>el eliminador del tipo que permite construir funciones cuyo dominio son las naturales y cuyo codominio es otra cosa. En otras palabras, es el principio de recursi\u00f3n.<\/li>\n<\/ul>\n<\/li>\n<li>En Lean, la propia igualdad se define como un tipo inductivo\n<pre class=\"example\">inductive eq {X : Type} : X \u2192 X \u2192 Prop\n| refl (a : X) : eq a a\n<\/pre>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgecac7fc\" class=\"outline-3\">\n<h3 id=\"orgecac7fc\"><span class=\"section-number-3\">4.3.<\/span> Las proposiciones son tipos<\/h3>\n<div id=\"text-4-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Una proposici\u00f3n es un tipo y sus pruebas son sus t\u00e9rminos.<\/li>\n<li>La hip\u00f3tesis h de que P implica Q se convierte en una funci\u00f3n h : P \u2192 Q.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd15809a\" class=\"outline-3\">\n<h3 id=\"orgd15809a\"><span class=\"section-number-3\">4.4.<\/span> Las pruebas son funciones<\/h3>\n<div id=\"text-4-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Nueva forma de pensar en la naturaleza de una prueba: se trata de una funci\u00f3n que toma como entrada las hip\u00f3tesis del resultado que se afirma, y devuelve como salida una prueba del resultado.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org421207e\" class=\"outline-3\">\n<h3 id=\"org421207e\"><span class=\"section-number-3\">4.5.<\/span> Un ejemplo<\/h3>\n<div id=\"text-4-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Enunciado:\n<div class=\"org-src-container\">\n<pre class=\"src src-lean\">example (n : \u2115) : (\u2211 i in range n, i^3 : \u211a) = ((n-1)*n\/2)^2 :=\nsorry\n<\/pre>\n<\/div>\n<\/li>\n<li>Demostraci\u00f3n (se encuentra <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#code=--%20use%20Lean's%20tactics%0Aimport%20tactic%0A%0A--%20enable%20sum%20notation%0Aopen_locale%20big_operators%0A%0A--%20use%20the%20theory%20of%20finite%20sets%0Aopen%20finset%0A%0Aexample%20%28n%20%3A%20%E2%84%95%29%20%3A%20%28%E2%88%91%20i%20in%20range%20n%2C%20i%5E3%20%3A%20%E2%84%9A%29%20%3D%20%28%28n-1%29*n%2F2%29%5E2%20%3A%3D%0Abegin%0A%20%20--%20Proof%20by%20induction%20on%20n%0A%20%20induction%20n%20with%20d%20hd%2C%0A%20%20%7B%20--%20base%20case%20can%20be%20done%20by%20tidying%20up%0A%20%20%20%20simp%2C%20ring%20%7D%2C%0A%20%20%7B%20--%20inductive%20step%3A%20a%20sum%20over%20%60range%20n%2B1%60%20is%20%0A%20%20%20%20--%20a%20sum%20over%20%60range%20n%60%20plus%20the%20%28n%2B1%29st%20term.%0A%20%20%20%20rewrite%20sum_range_succ%2C%0A%20%20%20%20--%20Now%20use%20our%20inductive%20hypothesis%0A%20%20%20%20rewrite%20hd%2C%0A%20%20%20%20--%20now%20tidy%20up%0A%20%20%20%20simp%2C%20ring%20%7D%0Aend%0A\">aqu\u00ed<\/a>)\n<div class=\"org-src-container\">\n<pre class=\"src src-lean\">-- use Lean's tactics\nimport tactic\n\nopen_locale big_operators\n\nopen finset\n\nexample (n : \u2115) : (\u2211 i in range n, i^3 : \u211a) = ((n-1)*n\/2)^2 :=\nbegin\n  induction n with d hd,\n  { simp, ring },\n  { rewrite sum_range_succ,\n    rewrite hd,\n    simp, ring }\nend\n<\/pre>\n<\/div>\n<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org7f77a7e\" class=\"outline-3\">\n<h3 id=\"org7f77a7e\"><span class=\"section-number-3\">4.6.<\/span> Fundamentos<\/h3>\n<div id=\"text-4-6\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Los matem\u00e1ticos suelen tener muy poco inter\u00e9s en los tecnicismos de los fundamentos l\u00f3gicos de su materia.<\/li>\n<li>Las controversias de principios del siglo XX sobre si los m\u00e9todos no constructivos est\u00e1n permitidos en las demostraciones matem\u00e1ticas han desaparecido hace tiempo.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgc18d4f9\" class=\"outline-2\">\n<h2 id=\"orgc18d4f9\"><span class=\"section-number-2\">5.<\/span> El futuro<\/h2>\n<div id=\"text-5\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-orgd38fd80\" class=\"outline-3\">\n<h3 id=\"orgd38fd80\"><span class=\"section-number-3\">5.1.<\/span> Un nuevo tipo de documento matem\u00e1tico<\/h3>\n<div id=\"text-5-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>La formalizaci\u00f3n ofrece la posibilidad de un nuevo tipo de documento matem\u00e1tico, en el que el lector puede decidir qu\u00e9 cantidad de detalles son visibles.<\/li>\n<li>Tambi\u00e9n se podr\u00eda imaginar que los libros de texto del grado se escribieran de esta manera, en la que las afirmaciones que un estudiante no pueda entender (quiz\u00e1s por ser ambiguas) puedan ser inspeccionadas con m\u00e1s detalle hasta que se resuelvan las dificultades.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9917f47\" class=\"outline-3\">\n<h3 id=\"org9917f47\"><span class=\"section-number-3\">5.2.<\/span> B\u00fasqueda sem\u00e1ntica en una base de datos matem\u00e1tica<\/h3>\n<div id=\"text-5-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Algo que no va a ocurrir pronto es que todos los matem\u00e1ticos empiecen a escribir todos sus trabajos en un asistente de pruebas formal.<\/li>\n<li>se puede esperar un futuro en el que algunos trabajos se formalicen parcialmente, o incluso completamente, en un demostrador de teoremas.<\/li>\n<li>Hales aboga por una versi\u00f3n formalizada de Math Reviews\/Zentralblatt. Es decir, un sitio web cuya funci\u00f3n sea simplemente exponer formalmente los resultados que se anuncian en las principales revistas de matem\u00e1ticas.<\/li>\n<li>El problema con el plan de Hales es que para poder formalizar los enunciados de los teoremas habr\u00eda que definir todos los objetos b\u00e1sicos que se utilizan.<\/li>\n<li>La comunidad de Lean se ha esforzado por introducir en mathlib algunas de las principales definiciones de la matem\u00e1tica de investigaci\u00f3n moderna.<\/li>\n<li>Un proyecto relacionado es la formalizaci\u00f3n de etiquetas en el <a href=\"https:\/\/stacks.math.columbia.edu\/\">Proyecto Stacks<\/a>: una gigantesca base de datos en l\u00ednea de geometr\u00eda algebraica, de libre acceso en l\u00ednea.<\/li>\n<li>Formalizar todas las pruebas del Proyecto Stacks no es una idea factible. Sin embargo, formalizar s\u00f3lo las definiciones y el estado de los teoremas es una tarea absolutamente accesible.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org6ffdb23\" class=\"outline-3\">\n<h3 id=\"org6ffdb23\"><span class=\"section-number-3\">5.3.<\/span> Comprobaci\u00f3n de pruebas<\/h3>\n<div id=\"text-5-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Lo que es factible es formalizar partes de la pruebas de grandes teoremas.<\/li>\n<li>Los demostradores de teoremas pueden utilizarse para comprobar pruebas que los humanos podr\u00edan considerar tediosas.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgf62f921\" class=\"outline-3\">\n<h3 id=\"orgf62f921\"><span class=\"section-number-3\">5.4.<\/span> La ense\u00f1anza<\/h3>\n<div id=\"text-5-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Deber\u00edamos ense\u00f1ar a los estudiantes universitarios a utilizar los asistentes de pruebas.<\/li>\n<li>Los demostradores deben ser m\u00e1s f\u00e1ciles de usar, quiz\u00e1s con interfaces gr\u00e1ficas y documentaci\u00f3n m\u00e1s apropiada para los matem\u00e1ticos.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgfb21f71\" class=\"outline-3\">\n<h3 id=\"orgfb21f71\"><span class=\"section-number-3\">5.5.<\/span> Otras ideas<\/h3>\n<div id=\"text-5-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li>Es hora de mirar m\u00e1s all\u00e1 de c\u00f3mo solemos ense\u00f1ar y aprender matem\u00e1ticas, y tratar de entender c\u00f3mo nosotros, como comunidad de matem\u00e1ticos, podemos utilizar la inevitable digitalizaci\u00f3n del material matem\u00e1tico como una herramienta para mejorar nuestras vidas, y las de nuestros estudiantes.<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobe razonamiento formalizado titulado What is the point of computers? A question for pure mathematicians. Su autor es Kevin Buzzard (Imperial College in London, U.K.). Su resumen es We discuss the idea that computers might soon help pure mathematicians to prove theorems in areas where they have not previously been&#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],"tags":[],"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\/7618"}],"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=7618"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7618\/revisions"}],"predecessor-version":[{"id":7624,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7618\/revisions\/7624"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7618"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7618"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7618"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}