dxdt.blog: занимательный интернет-журнал

Между прочим, через пару дней Mars Reconnaissance Orbiter (MRO) должен встать на марсианскую орбиту. На борту MRO, с целью фотографирования поверхности Марса, здоровенная камера HiRISE, каких раньше к другим планетам не отправляли:

(Длина камеры – около полутора метров)

Общещают длиные полоски снимков высокого разрешения (полоски, потому как камера снимает “вдоль” полета аппарата-носителя). На сайте камеры HiRISE есть программа для просмотра сих снимков, кои должны “развивать” разрешающую способность до трех пикселей на метр загадочной марсианской пустыни.

Вот интересное: http://www.emulator3000.org/rus-c3.htm – эмулятор советских программируемых калькуляторов. Тех самых, для которых печатались в журнале “Техника молодежи” забавные программы “калькуляторных игр”, снабженные фантастическим сюжетом в виде рассказа. Отсканированные страницы из журнала, с теми самыми рассказами и программами тоже имеются на сайте.

(via)

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

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

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

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

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

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

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