Интернациональная команда математиков во главе с доктором наук Питтсбургского университета Томасом Хейлзом поставила формальное подтверждение предположения Кеплера, известной неприятности в дискретной геометрии. Работа команды размещена в издании Forum of Mathematics, Пи.Доктор наук Хейлз демонстрирует собственный ответ предположения Кеплера. Кредит изображения: Боб Кэлмбак / Мичиганский университет.
Эссе ‘По шестиугольной снежинке’, которая была написана германским астрологом Йоханнесом Кеплером в 1611, содержит заявление того, что сейчас известно как предположение Кеплера: ‘ни у какой упаковки подходящих шаров в Евклидовом, с тремя пространствами, нет плотности, больше, чем та из гранецентрированной кубической упаковки’.Эта предположение – самая ветхая неприятность в дискретной геометрии.Ответ на предположение Кеплера, тогда как не тяжёлый предположить, было страно тяжело доказать.Доктор наук Хейлз и его студент Сэм Фергюсон первоначально заявили о доказательстве в 1998, но ответ было таким долгим и усложнило это, команда дюжины рефери совершила годы, трудясь над проверкой его перед отказом.
“Вердикт рефери был то, что подтверждение, казалось, трудилось, но у них просто не было времени либо энергии проверить все всесторонне”, сообщил Генри Кон, редактор Форума Математики, Пи и главного исследователя в Микрософт Research New England в Кембридже, Массачусетс.“Подтверждение было издано в 2005, и никакие непоправимые недочёты ни при каких обстоятельствах не определялись, но это была неудовлетворительная обстановка, что подтверждение было по-видимому вне способности сообщества математики проверить всецело”.
“Дабы обратиться к данной ситуации и установить уверенность, доктор наук Хейлз обратился к компьютерам, применяя способы формальной проверки”, растолковал Кон.“Он и команда сотрудников выписали все подтверждение в феноменальных подробностях, применяя строгую формальную логику, которая компьютерная программа тогда сверилась с красивой суровостью”.
Бумага не только улаживает вековую математическую проблему, но и есть кроме этого серьёзным шагом вперед в компьютерной проверке сложных математических доказательств.