{"id":151143,"date":"2026-02-20T20:44:47","date_gmt":"2026-02-20T19:44:47","guid":{"rendered":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/?p=151143"},"modified":"2026-02-20T20:44:47","modified_gmt":"2026-02-20T19:44:47","slug":"la-conjetura-de-kepler-e-isabelle","status":"publish","type":"post","link":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143","title":{"rendered":"La conjetura de Kepler e Isabelle"},"content":{"rendered":"

En la entrada previa<\/a>, hablamos de la conjetura de Kepler y como fue resuelta por Thomas Hales, con la ayuda de los ordenadores. Vamos ahora a comentar cu\u00e1l fue en concreto esa ayuda.<\/p>\n

\"\"<\/a><\/p>\n

Como dec\u00edamos, en enero de 2003, Hales anunci\u00f3 el inicio de un proyecto colaborativo para producir una prueba formal completa de la conjetura de Kepler, a fin de eliminar cualquier incertidumbre que pudiera quedar sobre la misma. Lo que ten\u00eda en la cabeza era crear una prueba formal que pudiera verificarse con software de comprobaci\u00f3n de pruebas automatizado, como HOL Light e Isabelle.<\/p>\n

Este proyecto se denomin\u00f3 Flyspeck, una ampliaci\u00f3n del acr\u00f3nimo FPK, que significa \u00abFormal Proof of Kepler\u00bb (Prueba formal de Kepler). Al inicio de este proyecto, en 2007, Hales estim\u00f3 que producir una prueba formal completa llevar\u00eda alrededor de 20 a\u00f1os de trabajo, sin embargo, la finalizaci\u00f3n del proyecto se anunci\u00f3 el 10 de agosto de 2014. En efecto, Hales y 21 colaboradores publicaron un art\u00edculo titulado \u00abA formal proof of the Kepler conjecture\u00bb (Una prueba formal de la conjetura de Kepler) en arXiv, en el que afirmaban haber demostrado la conjetura, y en 2017, la prueba formal fue aceptada por la revista Forum of Mathematics.<\/p>\n

\"\"<\/a>
Lawrence Paulson<\/figcaption><\/figure>\n

El demostrador autom\u00e1tico de teoremas Isabelle es un demostrador de teoremas de l\u00f3gica de orden superior HOL, acr\u00f3nimo de Higher-Order Logic, que es un lenguaje fuertemente tipado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones l\u00f3gicas con cuantificadores. A principios de la d\u00e9cada de 1980, Larry Paulson desarroll\u00f3 Cambridge LCF bas\u00e1ndose en trabajos anteriores de Robin Milner. Lawrence Charles Paulson es un inform\u00e1tico estadounidense, profesor de L\u00f3gica Computacional en el Laboratorio de Inform\u00e1tica de la Universidad de Cambridge.HOL es esencialmente el LCF de Cambridge con una l\u00f3gica diferente (l\u00f3gica de orden superior).  Isabelle estaba escrito en Standard ML y Scala. Standard ML (SML) es un lenguaje de programaci\u00f3n funcional modular, de alto nivel y uso general con comprobaci\u00f3n de tipos en tiempo de compilaci\u00f3n e inferencia de tipos. Scala, por su parte, es un lenguaje de programaci\u00f3n de alto nivel, fuertemente tipado y de prop\u00f3sito general, que admite tanto la programaci\u00f3n orientada a objetos como la programaci\u00f3n funcional.<\/p>\n

\"\"<\/a><\/p>\n

Isabelle est\u00e1 disponible dentro de un marco de sistema flexible que permite extensiones l\u00f3gicamente seguras, que comprenden tanto teor\u00edas como implementaciones para la generaci\u00f3n de c\u00f3digo, la documentaci\u00f3n y el soporte espec\u00edfico para una variedad de m\u00e9todos formales. Se puede considerar como un entorno de desarrollo integrado (IDE) para m\u00e9todos formales.<\/p>\n

En los \u00faltimos a\u00f1os, se ha recopilado un n\u00famero considerable de teor\u00edas y extensiones del sistema en el Archivo Isabelle de Pruebas Formales (Isabelle AFP).<\/p>\n

\"\"<\/a>
G\u00e9rard Pierre Huet<\/figcaption><\/figure>\n

Como curiosidad, digamos que Isabelle fue bautizada as\u00ed por Larry Paulson en honor a la hija de G\u00e9rard Pierre Huet, inform\u00e1tico, ling\u00fcista y matem\u00e1tico franc\u00e9s, director de investigaci\u00f3n s\u00e9nior en el INRIA (Institut national de recherche en informatique et en automatique<\/a>) y conocido principalmente por sus importantes y fundamentales contribuciones a la teor\u00eda de tipos, la teor\u00eda de los lenguajes de programaci\u00f3n y la teor\u00eda de la computaci\u00f3n.<\/p>\n

_____________<\/strong><\/p>\n

Manuel de Le\u00f3n<\/strong> (CSIC, Fundador del ICMAT, Real Academia de Ciencias, Real Academia Canaria de Ciencias, Real Academia Galega de Ciencias, Presidente del ICM2006 Madrid y miembro del Comit\u00e9 Ejecutivo de IMU (2007-2024) y del Comit\u00e9 Ejecutivo del ISC (2014-2018).<\/p>\n","protected":false},"excerpt":{"rendered":"

En la entrada previa, hablamos de la conjetura de Kepler y como fue resuelta por Thomas Hales, con la ayuda de los ordenadores. Vamos ahora a comentar cu\u00e1l fue en concreto esa ayuda. Como dec\u00edamos, en enero de 2003, Hales anunci\u00f3 el inicio de un proyecto colaborativo para producir una prueba formal completa de la conjetura de Kepler, a fin de eliminar cualquier incertidumbre que pudiera quedar sobre la misma. Lo que ten\u00eda en la cabeza era crear una prueba formal que pudiera verificarse con software de comprobaci\u00f3n de pruebas automatizado, como HOL Light e Isabelle. Este proyecto se denomin\u00f3\u2026<\/p>\n","protected":false},"author":49,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ngg_post_thumbnail":0},"categories":[1],"tags":[38832,49707,49706],"blocksy_meta":{"styles_descriptor":{"styles":{"desktop":"","tablet":"","mobile":""},"google_fonts":[],"version":4}},"aioseo_notices":[],"yoast_head":"\nLa conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143\" \/>\n<meta property=\"og:locale\" content=\"es_ES\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"La conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras\" \/>\n<meta property=\"og:description\" content=\"En la entrada previa, hablamos de la conjetura de Kepler y como fue resuelta por Thomas Hales, con la ayuda de los ordenadores. Vamos ahora a comentar cu\u00e1l fue en concreto esa ayuda. Como dec\u00edamos, en enero de 2003, Hales anunci\u00f3 el inicio de un proyecto colaborativo para producir una prueba formal completa de la conjetura de Kepler, a fin de eliminar cualquier incertidumbre que pudiera quedar sobre la misma. Lo que ten\u00eda en la cabeza era crear una prueba formal que pudiera verificarse con software de comprobaci\u00f3n de pruebas automatizado, como HOL Light e Isabelle. Este proyecto se denomin\u00f3\u2026\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143\" \/>\n<meta property=\"og:site_name\" content=\"Matem\u00e1ticas y sus fronteras\" \/>\n<meta property=\"article:published_time\" content=\"2026-02-20T19:44:47+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Escrito por\" \/>\n\t<meta name=\"twitter:data1\" content=\"Matem\u00e1ticas y sus fronteras\" \/>\n\t<meta name=\"twitter:label2\" content=\"Tiempo de lectura\" \/>\n\t<meta name=\"twitter:data2\" content=\"3 minutos\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#website\",\"url\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/\",\"name\":\"Matem\u00e1ticas y sus fronteras\",\"description\":\"\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"es\"},{\"@type\":\"ImageObject\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#primaryimage\",\"inLanguage\":\"es\",\"url\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png\",\"contentUrl\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png\",\"width\":994,\"height\":814},{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#webpage\",\"url\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143\",\"name\":\"La conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras\",\"isPartOf\":{\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#primaryimage\"},\"datePublished\":\"2026-02-20T19:44:47+00:00\",\"dateModified\":\"2026-02-20T19:44:47+00:00\",\"author\":{\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#\/schema\/person\/15722bca1b77eece37f4c192bd1b5230\"},\"breadcrumb\":{\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#breadcrumb\"},\"inLanguage\":\"es\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Portada\",\"item\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"La conjetura de Kepler e Isabelle\"}]},{\"@type\":\"Person\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#\/schema\/person\/15722bca1b77eece37f4c192bd1b5230\",\"name\":\"Matem\u00e1ticas y sus fronteras\",\"image\":{\"@type\":\"ImageObject\",\"@id\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#personlogo\",\"inLanguage\":\"es\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/50eb6cc40d97cb9ad268a3471c7e2492?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/50eb6cc40d97cb9ad268a3471c7e2492?s=96&d=mm&r=g\",\"caption\":\"Matem\u00e1ticas y sus fronteras\"},\"description\":\"Manuel de Le\u00f3n es Profesor de Investigaci\u00f3n del CSIC, acad\u00e9mico de la Real Academia de Ciencias y su Tesorero, fundador del ICMAT (CSIC), acad\u00e9mico de la Real Academia Canaria de Ciencias y de la Real Academia Galega de Ciencias. Es adem\u00e1s Director del programa Estalmat.\",\"url\":\"https:\/\/www.madrimasd.org\/blogs\/matematicas\/author\/matematicas\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"La conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143","og_locale":"es_ES","og_type":"article","og_title":"La conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras","og_description":"En la entrada previa, hablamos de la conjetura de Kepler y como fue resuelta por Thomas Hales, con la ayuda de los ordenadores. Vamos ahora a comentar cu\u00e1l fue en concreto esa ayuda. Como dec\u00edamos, en enero de 2003, Hales anunci\u00f3 el inicio de un proyecto colaborativo para producir una prueba formal completa de la conjetura de Kepler, a fin de eliminar cualquier incertidumbre que pudiera quedar sobre la misma. Lo que ten\u00eda en la cabeza era crear una prueba formal que pudiera verificarse con software de comprobaci\u00f3n de pruebas automatizado, como HOL Light e Isabelle. Este proyecto se denomin\u00f3\u2026","og_url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143","og_site_name":"Matem\u00e1ticas y sus fronteras","article_published_time":"2026-02-20T19:44:47+00:00","og_image":[{"url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png"}],"twitter_card":"summary_large_image","twitter_misc":{"Escrito por":"Matem\u00e1ticas y sus fronteras","Tiempo de lectura":"3 minutos"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebSite","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#website","url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/","name":"Matem\u00e1ticas y sus fronteras","description":"","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"es"},{"@type":"ImageObject","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#primaryimage","inLanguage":"es","url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png","contentUrl":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/files\/2026\/02\/Isabelle_jedit.png","width":994,"height":814},{"@type":"WebPage","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#webpage","url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143","name":"La conjetura de Kepler e Isabelle - Matem\u00e1ticas y sus fronteras","isPartOf":{"@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#primaryimage"},"datePublished":"2026-02-20T19:44:47+00:00","dateModified":"2026-02-20T19:44:47+00:00","author":{"@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#\/schema\/person\/15722bca1b77eece37f4c192bd1b5230"},"breadcrumb":{"@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#breadcrumb"},"inLanguage":"es","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/02\/20\/151143#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Portada","item":"https:\/\/www.madrimasd.org\/blogs\/matematicas"},{"@type":"ListItem","position":2,"name":"La conjetura de Kepler e Isabelle"}]},{"@type":"Person","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#\/schema\/person\/15722bca1b77eece37f4c192bd1b5230","name":"Matem\u00e1ticas y sus fronteras","image":{"@type":"ImageObject","@id":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/#personlogo","inLanguage":"es","url":"https:\/\/secure.gravatar.com\/avatar\/50eb6cc40d97cb9ad268a3471c7e2492?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/50eb6cc40d97cb9ad268a3471c7e2492?s=96&d=mm&r=g","caption":"Matem\u00e1ticas y sus fronteras"},"description":"Manuel de Le\u00f3n es Profesor de Investigaci\u00f3n del CSIC, acad\u00e9mico de la Real Academia de Ciencias y su Tesorero, fundador del ICMAT (CSIC), acad\u00e9mico de la Real Academia Canaria de Ciencias y de la Real Academia Galega de Ciencias. Es adem\u00e1s Director del programa Estalmat.","url":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/author\/matematicas"}]}},"_links":{"self":[{"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/posts\/151143"}],"collection":[{"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/users\/49"}],"replies":[{"embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/comments?post=151143"}],"version-history":[{"count":3,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/posts\/151143\/revisions"}],"predecessor-version":[{"id":151150,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/posts\/151143\/revisions\/151150"}],"wp:attachment":[{"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/media?parent=151143"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/categories?post=151143"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/wp-json\/wp\/v2\/tags?post=151143"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}