Ordenadores para una demostraci¨®n de Kepler

El problema al apilar naranjas, o balas de ca?¨®n, o bolas de billar, del modo m¨¢s eficaz es obvio: la disposici¨®n piramidal permite asentar m¨¢s abajo cada capa de naranjas, en el hueco dejado por la capa inferior, y ocupar menos espacio que si los frutos se asentaran unos encima de otros. Aunque ¨¦sa parec¨ªa la respuesta correcta, nadie ofreci¨® una demostraci¨®n matem¨¢tica convincente hasta 1998; e incluso entonces muchos expertos no quedaron convencidos. Durante seis a?os, los matem¨¢ticos han escudri?ado los cientos de p¨¢ginas de un art¨ªculo escrito por Thomas C. Hales, catedr¨¢tico de Matem¨¢ticas de la Universidad de Pittsburgh.

Pero la demostraci¨®n que Hales da al problema, conocido como la Conjetura de Kepler, se basa en una compleja serie de c¨¢lculos inform¨¢ticos; demasiados y demasiado tediosos para que los matem¨¢ticos que revisan su art¨ªculo los comprueben a mano. Creerla requiere, por consiguiente, cierto nivel de fe en que el ordenador realiz¨® los c¨¢lculos de manera intachable, sin errores de programaci¨®n. Para un campo que ofrece l¨®gica desapasionada y verdades y mentiras supuestamente inequ¨ªvocas, ¨¦se es un inc¨®modo intermedio gris¨¢ceo.

"La mente humana nunca ser¨¢ reemplazada", opina Larry Wos

El primer grupo de revisi¨®n dedic¨® varios a?os al intento, pero abandon¨® hace un a?o

Dadas las ambig¨¹edades, la revista, la prestigiosa Annals of Mathematics, ha decidido publicar s¨®lo las partes te¨®ricas de la demostraci¨®n, que se han comprobado de la manera tradicional. Una revista m¨¢s especializada, Discrete and Computational Geometry, publicar¨¢ los cap¨ªtulos inform¨¢ticos. La decisi¨®n representa un t¨¦rmino medio entre la aceptaci¨®n incondicional y el rechazo de las t¨¦cnicas inform¨¢ticas, cada vez m¨¢s habituales en matem¨¢ticas.

El debate sobre las demostraciones obtenidas con ayuda del ordenador es la versi¨®n superior de las discusiones sobre el uso de las calculadoras en las clases de matem¨¢ticas: si la tecnolog¨ªa genera mejores resultados, al acelerar los c¨¢lculos repetitivos, o si m¨¢s bien priva a las personas de su base. "No me gusta, porque uno no tiene la sensaci¨®n de entender lo que est¨¢ ocurriendo", afirma John H. Conway, catedr¨¢tico de Matem¨¢ticas en Princeton. Pero otros matem¨¢ticos consideran la inform¨¢tica una gran ayuda: de la misma forma que los ordenadores de hoy pueden vencer a los grandes maestros del ajedrez, los ordenadores del ma?ana quiz¨¢ puedan descubrir demostraciones con las que no han conseguido dar los mayores matem¨¢ticos.

El problema del almacenamiento de naranjas data al menos de la d¨¦cada de 1590, cuando sir Walter Raleigh, abasteciendo su barco para una expedici¨®n, se pregunt¨® si habr¨ªa una forma r¨¢pida de calcular el n¨²mero de balas de ca?¨®n acumuladas en una pila bas¨¢ndose en la altura de ¨¦sta. Su ayudante, Thomas Harriot, le proporcion¨® la ecuaci¨®n solicitada. A?os m¨¢s tarde, Harriot mencion¨® el problema a Johannes Kepler, el astr¨®nomo que hab¨ªa deducido el movimiento de los planetas.

Kepler concluy¨® que la pir¨¢mide era la forma m¨¢s eficaz (una disposici¨®n alternativa, con cada capa de esferas acumulada en forma de panal de abeja, es igualmente eficaz, pero no mejor). Pero Kepler no ofreci¨® una demostraci¨®n. Una demostraci¨®n rigurosa, noci¨®n establecida por primera vez por Euclides hacia el 300 a. C., es una progresi¨®n l¨®gica, que parte de suposiciones y llega a una conclusi¨®n. Si la cadena es correcta, la demostraci¨®n es verdadera, si no, es err¨®nea. Pero a veces una demostraci¨®n es un concepto borroso, sometido al capricho y a la personalidad. Casi ninguna demostraci¨®n publicada contiene todos los pasos; simplemente hay demasiados.

La Conjetura de Kepler tampoco es la primera demostraci¨®n basada en los ordenadores. En 1976, Wolfgang Haken y Kenneth Apel, de la Universidad de Illinois, usaron c¨¢lculos inform¨¢ticos para demostrar el teorema que afirma que cualquier mapa necesita s¨®lo cuatro colores para garantizar que no haya regiones adyacentes del mismo color. El trabajo se public¨®, y los matem¨¢ticos empezaron a encontrar errores en ¨¦l. En cada caso, Haken y Appel solucionaron r¨¢pidamente el error. Pero "a muchos matem¨¢ticas esto les dej¨® mal sabor de boca", dice Robert D. MacPherson, director de Annals.

Para evitar que esto volviera a suceder, los directores de Annals pidieron una revisi¨®n cuidadosa y completa de la demostraci¨®n de Hales. "Pero las cosas no han salido como esper¨¢bamos", dice MacPherson. El primer grupo de revisi¨®n dedic¨® varios a?os al intento, pero abandon¨® hace un a?o, agotado. Todo lo comprobado por los revisores, dirigidos por Gabor Fejes Toth, de la Academia H¨²ngara de Ciencias, result¨® correcto. Pero la perspectiva de revisar todos los c¨¢lculos result¨® demasiado abrumadora. MacPherson compara el proceso con corregir las pruebas de una gu¨ªa de tel¨¦fonos. "Todas las partes de la gu¨ªa de tel¨¦fonos que comprobaron estaban bien", dice, "y miraron en muchos sitios".

Los directores de Annals enviaron el art¨ªculo a otro matem¨¢tico, qui¨¦n confirm¨® que los fundamentos te¨®ricos eran buenos, y se tom¨® una decisi¨®n salom¨®nica: dividieron el art¨ªculo de Hales en dos. "La parte publicada en The Annals of Mathematics es una demostraci¨®n", dice MacPherson. "Consideramos que ha hecho una importante contribuci¨®n a las matem¨¢ticas".

Siguiendo una nueva pol¨ªtica, Annals ha decidido dar cr¨¦dito a las demostraciones asistidas por ordenador, pero con un valor inferior al otorgado a las demostraciones tradicionales, consider¨¢ndolas m¨¢s como experimentos de laboratorio que proporcionan pruebas suplementarias.

Incluso en las demostraciones tradicionales, los revisores raramente comprueban todos los pasos, centr¨¢ndose en los puntos m¨¢s importantes. Al final, pueden creerse o no la demostraci¨®n. "Cada vez m¨¢s personas dicen que ¨¦sa es la demostraci¨®n, y uno las cree", comenta Akihiro Kanamori, catedr¨¢tico de Matem¨¢ticas en la Universidad de Boston. Por eso hoy en d¨ªa rara vez se habla de una demostraci¨®n anterior de la Conjetura de Kepler, ofrecida ocho a?os antes que la de Hales. Wo-Yi Hsiang (Universidad de California en Berkeley), afirm¨® que ten¨ªa la demostraci¨®n en 1990, y en 1993 public¨® un art¨ªculo que ahora considera un borrador, no una demostraci¨®n completa. Los matem¨¢ticos la criticaron duramente, diciendo que conten¨ªa vac¨ªos de l¨®gica. Hsiang public¨® su demostraci¨®n completa en 2002 en forma de libro, no en una revista especializada.

Algunos creen que los ordenadores acallar¨¢n el debate sobre las demostraciones. En lugar de servir s¨®lo como herramientas para los c¨¢lculos, como en la demostraci¨®n de Hales, los ordenadores podr¨ªan usarse tambi¨¦n para descubrir nuevas demostraciones.

Matem¨¢ticos como Larry Wos, del Argonne National Laboratory, usan programas inform¨¢ticos de razonamiento automatizado: introducen los axiomas y el ordenador examina las posibilidades l¨®gicas en busca de una demostraci¨®n. Debido al enorme n¨²mero de posibilidades, sigue haciendo falta un humano para decirle al ordenador d¨®nde buscar. "La mente humana nunca ser¨¢ reemplazada", opina Wos, pero la ventaja de los ordenadores es su falta de ideas preconcebidas. "Pueden seguir trayectorias completamente opuestas a la intuici¨®n", dice. Considera que el ordenador tambi¨¦n realiza el trabajo tedioso, dando a los matem¨¢ticos m¨¢s tiempo para contemplar otros problemas, y genera tantos o tan pocos detalles como el matem¨¢tico desee. Intel, el gigante de los microprocesadores, usa programas de comprobaci¨®n de demostraciones para analizar los algoritmos de sus procesadores. Hales se ha embarcado en un proyecto similar, llamado Flyspeck las letras F, P y K hacen referencia a formal proof of Kepler

[demostraci¨®n formal de Kepler] para descartar todas las dudas que hoy provoca la demostraci¨®n inform¨¢tica. Sin embargo, los programas actuales no pueden manejar algo tan complejo como la Conjetura de Kepler. Hales calcula que para completar el proyecto har¨¢n falta 20 a?os de trabajo acumulativo de un equipo de matem¨¢ticos.

? The New York Times