Упаковка апельсинов бочками

Между прочим, раз тут зашел разговор, то Том Хейлз (Thomas C. Hales), механистически разобравшийся в 1998 году со старинной задачей Кеплера о наиболее плотной упаковке сфер, поддерживает целый проект по обоснованию своего доказательства с помощью специального формализма.

Хейлз подтвердил правильность данного Кеплером решения, частный случай которого давно применяется продавцами круглых апельсинов и известен даже Чебурашке (укладка апельсинов пирамидой, практиковалась этим персонажем).

Предположение же Кеплера, остававшееся недоказанным около четырехсот лет, заключалось в том, что максимально плотная упаковка сфер одинакового диаметра достигается при их гранецентрированной кубической укладке в ящик. Хейлз доказал, что это так, существенным образом использовав компьютерные вычисления. Именно из-за этих самых компьютерных вычислений, доказательство Хейлза так и не признано полностью, несмотря на то, что ему посвящали целые конференции.

Компьютерным программным кодам нет доверия.

Это правильно.

Но Хейлз поддерживает проект под названием Flyspeck. Вообще-то, flyspeck – английское название для “мушиного помета”, но по версии создателей проекта это всего лишь слово из словаря, подходящее под маску /f.*p.*k/ (где FPK – Formal Proof of Kepler).

Цель проекта – получение программной реализации некоего компьютерного “формализма”, оперирующего не какими-то “алгоритмами” и “данными”, а строгими теоремами (там есть и тип данных – theorem). Таким образом, планируется получение виртуально строгого, но, вместе с тем, компьютерного, вычислительного доказательства. Попутно обещают выкинуть все интуитивное из всех доказательств вообще. Вот так. Объем работы – двадцать человеко-лет.

()

Похожие записки:



Далее - мнения и дискуссии

(Сообщения ниже добавляются читателями сайта, через форму, расположенную в конце страницы.)

Комментарии читателей блога: 2

  • 1. 4th February 2008, 19:05 // Читатель dxdt.ru: занимательный… написал:

    […] результатов, или даже вообще первый. И из последних самый нашумевший вычислительный результат – это задача об укладке апельсинов. (Оценить запись)  Loading … Читайте […]

  • 2. 24th May 2008, 10:38 // Читатель zarges написал:

    тоже не верю