Предположение Кеплера была известной проблемой в дискретной геометрии, которая попросила самый действенный метод переполнить сферы в данное пространство. Ответ, тогда как не тяжёлый предположить (это совершенно верно, как апельсины сложены в супермаркете), было страно тяжело доказать. Хейлз и Фергюсон первоначально заявили о доказательстве в 1998, но ответ было таким долгим и усложнило это, команда дюжины рефери совершила годы, трудясь над проверкой его перед отказом.Растолковывает Генри Кон, редактор Форума Математики, Пи: «Вердикт рефери был то, что подтверждение, казалось, трудилось, но у них просто не было времени либо энергии проверить все всесторонне.
Подтверждение было издано в 2005, и никакие непоправимые недочёты ни при каких обстоятельствах не определялись, но это была неудовлетворительная обстановка, что подтверждение было по-видимому вне способности сообщества математики проверить всецело. Дабы обратиться к данной ситуации и установить уверенность, Хейлз обратился к компьютерам, применяя способы формальной проверки. Он и команда сотрудников выписали все подтверждение в феноменальных подробностях, применяя строгую формальную логику, которая компьютерная программа тогда сверилась с красивой суровостью. Эта статья – итог их законченной работы».
Томас Хейлз – доктор наук Меллона Математики в Питтсбургском университете. Его изучение охватывает дискретную геометрию, теорию представления, motivic формальное доказательство и интеграция теоремы.