Prueba de la conjetura de Kepler sobre empaquetamiento de esferas
Proof of the Kepler conjecture
- Fecha
- 1998 (verificación formal 2014) · fiabilidad alta
- Lugar
- Ann Arbor, Michigan, EE. UU.
- Autoría
- Thomas Hales (con Samuel Ferguson); proyecto Flyspeck (2014)
- Personas
- 👤 Thomas Callister Hales1958–
- Ámbito
- Saber y símbolos
Qué se descubrió
Ningún empaquetamiento de esferas iguales supera la densidad del apilamiento del frutero (pi/raíz de 18), como conjeturó Kepler en 1611. La prueba, con enorme cómputo, fue verificada formalmente en HOL Light e Isabelle en 2014.
Los referees de Annals declararon estar seguros al 99 por ciento, lo que motivó la formalización.
A qué dio paso
- verificación formal de grandes demostraciones
- empaquetamientos en dimensión 8 y 24 (Viazovska)
Se apoya en
- Teorema de los cuatro colores (primera prueba asistida por ordenador)1976
- Gauss (empaquetamientos reticulares)
- Fejes Tóth (estrategia, 1953)
Hizo posible
- diseño de códigos y cristalografía