En 1998, Thomas Hales , siguiendo un enfoque sugerido por Fejes Tóth (1953), anunció que tenía una prueba de la conjetura de Kepler. La prueba de Hales es una prueba por agotamiento que implica la verificación de muchos casos individuales mediante complejos cálculos informáticos. Los árbitros dijeron que estaban "99% seguros" de la exactitud de la prueba de Hales, y la conjetura de Kepler fue aceptada como un teorema . En 2014, el equipo del proyecto Flyspeck, encabezado por Hales, anunció la finalización de una prueba formal de la conjetura de Kepler utilizando una combinación de los asistentes de prueba Isabelle y HOL Light . En 2017, la prueba formal fue aceptada por la revista Forum of Mathematics, Pi . [1]
Fondo
Imagínese llenar un recipiente grande con pequeñas esferas del mismo tamaño: digamos una jarra de porcelana de un galón con canicas idénticas. La "densidad" del arreglo es igual al volumen total de todas las canicas, dividido por el volumen de la jarra. Maximizar el número de canicas en la jarra significa crear una disposición de canicas apiladas entre los lados y el fondo de la jarra, que tenga la mayor densidad posible, de modo que las canicas queden juntas lo más juntas posible.
Los experimentos muestran que dejar caer las canicas al azar, sin hacer ningún esfuerzo por colocarlas bien juntas, logra una densidad de alrededor del 65%. [2] Sin embargo, se puede lograr una mayor densidad disponiendo cuidadosamente las canicas de la siguiente manera:
Para la primera capa de canicas, colóquelas en una red hexagonal ( el patrón de panal ).
Coloque la siguiente capa de canicas en los espacios más bajos que pueda encontrar arriba y entre las canicas de la primera capa, independientemente del patrón.
Continúe con el mismo procedimiento de rellenar los espacios más bajos de la capa anterior, para la tercera capa y las restantes, hasta que las canicas lleguen al borde superior de la jarra.
En cada paso hay al menos dos opciones sobre cómo colocar la siguiente capa, por lo que este método no planificado de apilar las esferas crea un número infinito e incontable de empaquetamientos igualmente densos. Los más conocidos se denominan empaquetamiento cerrado cúbico y empaquetamiento 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: ningún otro arreglo de canicas tiene una densidad promedio más alta: a pesar de que hay asombrosamente muchos arreglos diferentes posibles que siguen el mismo procedimiento que los pasos 1 a 3, no se empaqueta (según la procedimiento o no) es posible que quepan más canicas en la misma jarra.
Orígenes
La conjetura fue expuesta por primera vez por Johannes Kepler (1611) en su artículo "Sobre el copo de nieve de seis puntas". Había comenzado a estudiar la disposición de 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 pedido que encontrara fórmulas para contar balas de cañón apiladas, una tarea lo que a su vez llevó a un conocido matemático de Raleigh a preguntarse cuál era la mejor manera de apilar balas de cañón. [3] 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 el siguiente paso lo dio Carl Friedrich Gauss (1831), quien demostró que la conjetura de Kepler es verdadera si las esferas tienen que estar dispuestas en una red regular .
Esto significaba que cualquier disposición de embalaje que refutara la conjetura de Kepler tendría que ser irregular. Pero eliminar todos los posibles arreglos irregulares es muy difícil, y esto es lo que hizo que la conjetura de Kepler fuera tan difícil de demostrar. De hecho, hay disposiciones irregulares que son más densas que la disposición cúbica cerrada en un volumen suficientemente pequeño, pero ahora se sabe que cualquier intento de extender estas disposiciones para llenar un volumen mayor siempre reduce su densidad.
El siguiente paso hacia una solución lo dio László Fejes Tóth . Fejes Tóth (1953) demostró que el problema de determinar la densidad máxima de todos los arreglos (regulares e irregulares) podía reducirse a un número finito (pero muy grande) de cálculos. Esto significaba que, en principio, era posible una prueba por agotamiento. Como se dio cuenta Fejes Tóth, una computadora lo suficientemente rápida podría convertir este resultado teórico en una aproximación práctica al problema.
Mientras tanto, se intentó encontrar un límite superior para la densidad máxima de cualquier posible disposición de esferas. El matemático inglés Claude Ambrose Rogers (ver Rogers (1958)) estableció un valor límite superior de aproximadamente el 78%, y los esfuerzos posteriores de otros matemáticos redujeron este valor ligeramente, pero aún era mucho mayor que la densidad cúbica de empaquetamiento cerrado de aproximadamente el 74%.
En 1990, Wu-Yi Hsiang afirmó haber demostrado la conjetura de Kepler. La prueba fue elogiada por Encyclopædia Britannica y Science y Hsiang también fue honrado en reuniones conjuntas de AMS-MAA. [4] Wu-Yi Hsiang (1993, 2001) afirmó haber demostrado la conjetura de Kepler utilizando métodos geométricos. Sin embargo, Gábor Fejes Tóth (hijo de László Fejes Tóth) afirmó en su reseña del artículo: "En lo que respecta a los detalles, mi opinión es que muchas de las afirmaciones clave no tienen pruebas aceptables". Hales (1994) hizo una crítica detallada del trabajo de Hsiang, a la que respondió Hsiang (1995). El consenso actual es que la prueba de Hsiang es incompleta. [5]
La prueba de Hales
Siguiendo el enfoque sugerido [6] por László Fejes Tóth , Thomas Hales , entonces en la Universidad de Michigan , determinó que la densidad máxima de todos los arreglos se podía encontrar minimizando una función con 150 variables. En 1992, con la ayuda de su estudiante de posgrado 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 del valor de esta función para cada una 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 cúbica cerrada, entonces se demostraría la conjetura de Kepler. Encontrar límites inferiores para todos los casos implicó resolver alrededor de 100.000 problemas de programación lineal.
Al presentar los avances 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 podían certificar la exactitud de todos los cálculos informáticos. .
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 partes computacionales. Hales y Ferguson recibieron el Premio Fulkerson por trabajos destacados en el área de matemáticas discretas en 2009.
Una prueba formal
En enero de 2003, Hales anunció el inicio de un proyecto colaborativo 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 software de verificación de pruebas automatizado como HOL Light e Isabelle . Este proyecto se llamó Flyspeck , una ampliación del acrónimo FPK que significa Prueba formal de Kepler . Al inicio de este proyecto, en 2007, Hales estimó que producir una prueba formal completa requeriría alrededor de 20 años de trabajo. [7] Hales publicó un "plan" para la prueba formal en 2012; [8] la finalización del proyecto se anunció el 10 de agosto de 2014. [9] En enero de 2015, Hales y 21 colaboradores publicaron un artículo titulado "Una prueba formal de la conjetura de Kepler" en arXiv , afirmando haber probado la conjetura. [10] En 2017, la prueba formal fue aceptada por la revista Forum of Mathematics . [1]
Problemas relacionados
Teorema de Thue
El empaquetamiento hexagonal regular es el empaquetamiento circular más denso del plano (1890). La densidad es π ⁄ √ 12 .
El análogo bidimensional de la conjetura de Kepler; la prueba es elemental. Henk y Ziegler atribuyen este resultado a Lagrange, en 1773 (véanse las referencias, pág. 770).
Una prueba sencilla de Chau y Chung de 2010 utiliza la triangulación de Delaunay para el conjunto de puntos que son centros de círculos en un paquete de círculos saturado. [11]
El volumen del poliedro de Voronoi de una esfera en un conjunto de esferas iguales es al menos el volumen de un dodecaedro regular con radio 1. Prueba de McLaughlin, [13] por la que recibió el Premio Morgan en 1999 .
Un problema relacionado, cuya prueba utiliza técnicas similares a la prueba de la conjetura de Kepler de Hales. Conjetura de L. Fejes Tóth en los años 1950.
¿Cuál es la espuma más eficiente en 3 dimensiones? Se conjeturó que esto se resolvería mediante la estructura Kelvin , y así se creyó ampliamente durante más de 100 años, hasta que fue refutado en 1993 por el descubrimiento de la estructura Weaire-Phelan . El sorprendente descubrimiento de la estructura de Weaire-Phelan y la refutación de la conjetura de Kelvin es una de las razones de la cautela al aceptar la prueba de Hales de la conjetura de Kepler.
En 2016, Maryna Viazovska anunció una prueba del empaquetamiento óptimo de esferas en la dimensión 8, lo que rápidamente condujo a una solución en la dimensión 24. [14] Sin embargo, la pregunta sobre el empaquetamiento óptimo de esferas en dimensiones distintas a 1, 2, 3, 8 y 24 todavía está abierto.
Se desconoce si existe un sólido convexo cuya densidad de empaquetamiento óptima sea menor que la de la esfera.
Referencias
^ ab Hales, Thomas ; Adams, Marcos; Bauer, Gertrud; Maldita sea, tat dat; Harrison, Juan; Hoang, Le Truong; Kaliszyk, Cézary; Magrón, Víctor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobías; Obua, Steven; Pleso, José; Ruta, Jason; Soloviev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urbano, José; Vu, Ky; Zumkeller, Roland (29 de mayo de 2017). "Una prueba formal de la conjetura de Kepler". Foro de Matemáticas, Pi . 5 : e2. doi : 10.1017/fmp.2017.1 . hdl : 2066/176365 .
^ Li, Shuixiang; Zhao, Liang; Liu, Yuewu (abril de 2008). "Simulación por computadora del embalaje de esferas aleatorias en un contenedor de forma arbitraria". Computadoras, Materiales y Continua . 7 : 109-118.
^ Leutwyler, Kristin (14 de septiembre de 1998). "Apílalos bien". Científico americano . Consultado el 15 de noviembre de 2021 .
^ Bails, Jennifer (otoño de 2007). "Thomas Hales: la prueba de la prueba". Pittsburgh trimestral .
^ Hales, Thomas C. (2012). Empaquetaduras de esferas densas: un modelo para pruebas formales . Serie de notas de conferencias de la Sociedad Matemática de Londres. vol. 400. Prensa de la Universidad de Cambridge. ISBN978-0-521-61770-3.
^ Hales, Thomas ; et al. (9 de enero de 2015). "Una prueba formal de la conjetura de Kepler". arXiv : 1501.02155 [matemáticas.MG].
^ Chang, Hai-Chau; Wang, Lih-Chung (22 de septiembre de 2010). "Una prueba simple del teorema de Thue sobre el embalaje circular". arXiv : 1009.4322 [matemáticas.MG].
^ Hales, Thomas C. (20 de mayo de 2002). "La conjetura del panal". Geometría discreta y computacional . 25 : 1–22. arXiv : matemáticas/9906042 . doi :10.1007/s004540010071. S2CID 14849112.
Gauss, Carl F. (1831), "Untersuchungen über die Eigenschaften der positivn ternären quadratischen Formen von Ludwig August Seeber", Göttingische gelehrte Anzeigen (108): 1065–1077
Hales, Thomas C. (2000), "Balas de cañón y panales", Avisos de la Sociedad Matemática Estadounidense , 47 (4): 440–449, ISSN 0002-9920, SEÑOR 1745624Una exposición elemental de la prueba de la conjetura de Kepler.
Hales, Thomas C. (2005), "Una prueba de la conjetura de Kepler", Annals of Mathematics , Segunda Serie, 162 (3): 1065–1185, arXiv : math/9811078 , doi :10.4007/annals.2005.162.1065, ISSN 0003-486X, SEÑOR 2179728
Hales, Thomas C. (2006), "Reseña histórica de la conjetura de Kepler", Geometría computacional y discreta , 36 (1): 5–20, doi : 10.1007/s00454-005-1210-2 , ISSN 0179-5376, SEÑOR 2229657
Hales, Thomas C.; Ferguson, Samuel P. (2006), "Una formulación de la conjetura de Kepler" (PDF) , Geometría computacional y discreta , 36 (1): 21–69, arXiv : math/9811078 , doi :10.1007/s00454-005-1211 -1, ISSN 0179-5376, SEÑOR 2229658, S2CID 6529590
Hales, Thomas C.; Ferguson, Samuel P. (2011), La conjetura de Kepler: la prueba de Hales-Ferguson , Nueva York: Springer, ISBN 978-1-4614-1128-4
Hales, Thomas C. (2012), "Empaquetaduras de esferas densas: un modelo para pruebas formales", Serie de notas de conferencias de la London Mathematical Society , 400 , Cambridge University Press, ISBN 978-0-521-61770-3
Henk, Martín; Ziegler, Guenther (2008), La congettura di Keplero , La matematica. Problemi e teoremi, vol. 2, Turín: Einaudi
Hsiang, Wu-Yi (1993), "Sobre el problema del empaquetamiento de esferas y la prueba de la conjetura de Kepler", Revista Internacional de Matemáticas , 4 (5): 739–831, doi :10.1142/S0129167X93000364, ISSN 0129-167X, MR 1245351
Hsiang, Wu-Yi (1995), "Una réplica al artículo de TC Hales: El estado de la conjetura de Kepler ", The Mathematical Intelligencer , 17 (1): 35–42, doi :10.1007/BF03024716, ISSN 0343-6993, SEÑOR 1319992, S2CID 119641512
Hsiang, Wu-Yi (2001), Principio de mínima acción de la formación de cristales de tipo empaquetamiento denso y conjetura de Kepler , Nankai Tracts in Mathematics, vol. 3, River Edge, Nueva Jersey: World Scientific Publishing Co. Inc., doi :10.1142/9789812384911, ISBN 978-981-02-4670-9, SEÑOR 1962807
Kepler, Johannes (1611), Strena seu de nive sexangula [ El copo de nieve de seis puntas ] (en latín), Paul Dry Books, ISBN 978-1-58988-053-5, señor 0927925
"Sobre el copo de nieve de seis esquinas". El descubrimiento de Kepler . Archivado desde el original el 19 de diciembre de 2007.
Marchal, Christian (2011), "Estudio de la conjetura de Kepler: el problema del embalaje más cercano", Mathematische Zeitschrift , 267 (3–4): 737–765, doi :10.1007/s00209-009-0644-2, S2CID 122088451
Rogers, CA (1958), "El embalaje de esferas iguales", Actas de la Sociedad Matemática de Londres , Tercera Serie, 8 (4): 609–620, doi :10.1112/plms/s3-8.4.609, ISSN 0024-6115 , SEÑOR 0102052
Fejes Tóth, L. (1953), Lagerungen in der Ebene, auf der Kugel und im Raum , Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Band LXV, Berlín, Nueva York: Springer-Verlag , doi :10.1007/ 978-3-642-65234-9, ISBN 978-3-642-65235-6, señor 0057566
Portada de 'Sobre el copo de nieve de seis puntas'
Página de inicio de Thomas Hales
Página de inicio del proyecto Flyspeck
Descripción general de la prueba de Hales Archivado el 27 de septiembre de 2011 en Wayback Machine.
Artículo en American Scientist por Dana Mackenzie
Flyspeck I: Tame Graphs, enumeración verificada de gráficos planos domesticados según lo define Thomas C. Hales en su prueba de la conjetura de Kepler.