Existen resultados cuyas demostraciones involucran una mezcla de razonamientos complejos con un gran número de cálculos. Un ejemplo de esto es la conjetura de Kepler, que establece que ninguna disposición de esferas sólidas e idénticas en el espacio tiene una densidad media mayor que la disposición cúbica o la hexagonal. La densidad media de estas disposiciones es de Pi / (raíz cuadrada de 18), que es aproximadamente 0.74. La conjetura fue enunciada primeramente por Kepler en 1611. Estuvo mas de 380 años sin resolverse; Hilbert la incluyó en su lista de los 23 problemas no resueltos (es una de las tres partes del problema número 18). Hubo numerosos intentos incorrectos de demostrar esta conjetura, hasta que en 1998 Tomas Hales anunció que su demostración estaba completa. Hales había anunciado previamente (en 1996) un esquema de la demostración exhaustiva que llevaría a cabo, y había explicado que llevaría un año o dos completarla. La demostración de Hales tenía 250 páginas y mas de 3 gigabytes de resultados. Después de 4 años de evaluación, el jurado determinó que estaban "99%" convencidos de que la prueba era correcta, pero que no podían asegurar la correctitud de los cálculos. En 2003 Hales anunció el comienzo del proyecto FlysPecK para producir una prueba formal de la conjetura. El objetivo de este proyecto es eliminar cualquier incerteza restante acerca de la validez de la demostración, creando una prueba que pueda ser verificada automáticamente con softwares como Coq. Muchos de los resultados pendientes de la demostración de Hales son lemas que afirman que ciertos polinomios son no negativos en cajas dadas. En este trabajo se presenta la primera parte de una contribución al proyecto FlysPecK, que pretende automatizar las demostraciones de esos lemas. Los teoremas "positivstellensatz" de Stengle y "nullstellensatz" de Hilbert servirán como fundamentos teóricos para el trabajo.