Conjetura de Kepler
La conjetura de Kepler fue formulada por el físico, matemático y astrónomo alemán Johannes Kepler en 1611. Esta conjetura afirma que si apilamos esferas iguales, la densidad máxima se alcanza con una apilamiento piramidal de caras centradas. Esta densidad es aproximadamente del 74%.
En 1998 Thomas Hales anunció que había demostrado la conjetura de Kepler. Fue publicada en Annals of Mathematics. La comprobación de Hales es una demostración por casos en la que se prueban agrupamientos mediante complejos cálculos de computadora (ordenador). Hales formuló una ecuación de 150 variables que recogía cinco mil posibles agrupamientos de esferas iguales.
Los doce científicos seleccionados por Annals para realizar la revisión por pares comentaron que estaban al "99% seguros" de la exactitud de la prueba de Hales, pero que era imposible revisar los tres gigabytes de códigos. Sin embargo, el método utilizado por Hales en la demostración no es exhaustivo, por lo que no está dilucidado el problema. Por tanto, la conjetura de Kepler está más cerca de convertirse en un teorema.
El autor de la solución se dedicó a crear el proyecto Flyspeck, consistente en un programa que verifica paso a paso todas las afirmaciones lógicas de la solución matemática, verificándola en lugar de los propios matemáticos. El 9 de agosto de 2014, el equipo de Hales anunció que el programa que crearon logró verificar la solución de la Conjetura de Kepler propuesta por Hales, y que no encontró errores.
“Esta tecnología excluye a los árbitros matemáticos del proceso de verificación. Su opinión sobre la corrección de las pruebas ya no importa más”, afirma Hales, citado por la revista ‘New Scientist‘. La prueba del problema, verificada por una computadora, puede abrir una nueva era en las matemáticas donde las máquinas harán el “trabajo pesado” liberando a los científicos para que se puedan dedicar al “pensamiento más profundo”.
En junio de 2017, la demostración formal de la Conjetura de Kepler fue aceptada en la revista Forum of Mathematics.[1]
Antecedentes
Imagine llenar un recipiente grande con esferas pequeñas del mismo tamaño. La densidad de la disposición es igual al volumen colectivo de las esferas dividido por el volumen del contenedor. Maximizar el número de esferas en el contenedor significa crear una disposición con la mayor densidad posible, de modo que las esferas se empaqueten juntas lo más cerca posible.
El experimento muestra que soltar las esferas al azar alcanzará una densidad de alrededor del 65%.[2] Sin embargo, se puede lograr una mayor densidad organizando cuidadosamente las esferas de la siguiente manera. Comience con una capa de esferas en una red hexagonal, luego coloque la siguiente capa de esferas en los puntos más bajos que pueda encontrar sobre la primera capa, y así sucesivamente. En cada paso hay dos opciones de dónde colocar la siguiente capa, por lo que este método natural de apilar las esferas crea un número infinitamente infinito de empaques igualmente densos, los más conocidos se denominan empaquetamiento cerrado cúbico y empaque cerrado hexagonal. Cada uno de estos arreglos tiene una densidad promedio de
La conjetura de Kepler dice que esto es lo mejor que se puede hacer: ninguna otra disposición de esferas tiene una densidad promedio más alta.
Orígenes
La conjetura fue declarada por primera vez por Johannes Kepler en su artículo "On the six-cornered snowflake" (Sobre el copo de nieve de seis picos). Había comenzado a estudiar los arreglos de las esferas como resultado de su correspondencia con el matemático y astrónomo inglés Thomas Harriot en 1606. Harriot era amigo y asistente de Sir Walter Raleigh, quien le había planteado a Harriot el problema de determinar la mejor manera de apilar balas de cañón en las cubiertas de sus barcos. Harriot publicó un estudio de varios patrones de apilamiento en 1591 y desarrolló una versión temprana de la teoría atómica.
Siglo XIX
Kepler no tenía una prueba de la conjetura, y Carl Friedrich Gauss (1831) dio el siguiente paso, quien demostró que la conjetura de Kepler es cierta si las esferas tienen que organizarse en una red regular.
Esto significaba que cualquier arreglo de empaque que refutara la conjetura de Kepler tendría que ser irregular. Pero eliminar todos los arreglos irregulares posibles es muy difícil, y esto es lo que hizo que la conjetura de Kepler fuera tan difícil de probar. De hecho, hay disposiciones irregulares que son más densas que la disposición de empaquetado cúbico cerrado en un volumen lo suficientemente pequeño, pero ahora se sabe que cualquier intento de extender estas disposiciones para llenar un volumen mayor siempre reduce su densidad.
Después de Gauss, no se hicieron más progresos para probar la conjetura de Kepler en el siglo XIX. En 1900, David Hilbert lo incluyó en su lista de veintitrés problemas matemáticos no resueltos; forma parte del decimoctavo problema de Hilbert.
Prueba de Hales
Siguiendo el enfoque sugerido por Fejes Tóth (1953), Thomas Hales, entonces en la Universidad de Míchigan, determinó que la densidad máxima de todos los arreglos se podía encontrar minimizando una función con 150 variables. En 1992, asistido por su estudiante graduado Samuel Ferguson, se embarcó en un programa de investigación para aplicar sistemáticamente métodos de programación lineal para encontrar un límite inferior en el valor de esta función para cada uno de un conjunto de más de 5.000 configuraciones diferentes de esferas. Si se pudiera encontrar un límite inferior (para el valor de la función) para cada una de estas configuraciones que fuera mayor que el valor de la función para la disposición de empaquetado cúbico cercano, entonces se demostraría la conjetura de Kepler. Encontrar límites inferiores para todos los casos involucrados en la resolución de aproximadamente 100.000 problemas de programación lineal.
Al presentar el progreso de su proyecto en 1996, Hales dijo que el final estaba a la vista, pero que podría llevar "uno o dos años" completarlo. En agosto de 1998, Hales anunció que la prueba estaba completa. En esa etapa, constaba de 250 páginas de notas y 3 gigabytes de programas informáticos, datos y resultados.
A pesar de la naturaleza inusual de la prueba, los editores de Annals of Mathematics acordaron publicarla, siempre que fuera aceptada por un panel de doce árbitros. En 2003, después de cuatro años de trabajo, el jefe del panel de árbitros, Gábor Fejes Tóth, informó que el panel estaba "99% seguro" de la exactitud de la prueba, pero no pudieron certificar la exactitud de todos los cálculos de la computadora.
Hales (2005) publicó un artículo de 100 páginas que describe en detalle la parte no informática de su prueba. Hales y Ferguson (2006) y varios artículos posteriores describieron las porciones computacionales. Hales y Ferguson recibieron el Premio Fulkerson por trabajos sobresalientes en el área de las matemáticas discretas para 2009.
Una prueba formal
En enero de 2003, Hales anunció el inicio de un proyecto de colaboración para producir una prueba formal completa de la conjetura de Kepler. El objetivo era eliminar cualquier incertidumbre restante sobre la validez de la prueba mediante la creación de una prueba formal que pueda verificarse mediante un software de verificación de pruebas automatizado como HOL Light e Isabelle. Este proyecto se llama Flyspeck, la F, P y K que significa Prueba Formal de Kepler. Hales estimó que producir una prueba formal completa tomaría alrededor de 20 años de trabajo. Hales publicó por primera vez un "plan" para la prueba formal en 2012;[3] El proyecto se anunció terminado el 10 de agosto de 2014.[4] En enero de 2015, Hales y 21 colaboradores presentaron un documento titulado "Una prueba formal de la conjetura de Kepler" a arXiv, alegando haber probado la conjetura.[5] En 2017, la prueba formal fue aceptada en la revista Forum of Mathematics.
Véase también
Referencias
- Thomas Hales et al. «A FORMAL PROOF OF THE KEPLER CONJECTURE». Consultado el 25 de junio de 2017.
- Li, Shuixiang; Zhao, Liang; Liu, Yuewu (April 2008). «Computer simulation of random sphere packing in an arbitrarily shaped container». Computers, Materials and Continua 7: 109-118.
- Hales, Thomas C. (2012). «Dense Sphere Packings: A Blueprint for Formal Proofs». London Mathematical Society Lecture Note Series 400 (Cambridge University Press). ISBN 978-0-521-61770-3.
- «Project Flyspeck». Google Code.
- Hales, Thomas (9 de enero de 2015). «A Formal Proof of the Kepler Conjecture». .
Enlaces externos
- Enlaces en castellano
- Matemáticalia
- Ejemplo práctico sobre la conjetura de Kepler
- Enlaces en inglés
- Thomas Hales' home page
- Overview of Hales' proof