Кстати, первое опровержение известной гипотезы Эйлера насчёт обобщения большой теоремы Ферма появилось в 1966-ом:

1445 = 1335+1105+845+275

Опровержение просто вычислили. Это оказался один из первых замечательных вычислительных результатов, или даже вообще первый. И из последних самый нашумевший вычислительный результат – это задача об укладке апельсинов.



Comments Off on Эйлер и числа

Забавно (специально для arbuz.uz Скляревского):

31138+20128+19538+8618=28238+27678+25578+11288

Там же: 224955952840404+75924319813914+272397916926404=299998579386094

(via)



Comments Off on Числа

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

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

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

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

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

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

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



Комментарии (2) »
Навигация по запискам: « Позже