Первая мысль -- бабель не работает.

Кто-то выложил её онлайн (http://en.wikipedia.org/wiki/Principia_Mathematica#External_links)
- 2000 страниц рукописного байт-кода, безумие.

Это я был. Рассел -- придурок (как мне кажется, это видно из его книжек), а Уайтхед довольно интересный.

Ты выложил онлайн - идейно, блин!

Ой :)

аспиранты наваяли ;)

Если бы аспиранты, то вышел бы и четвёртый том, про "Геометрию". А он не вышел - R и W пожаловались на истощение. Или, думаете, хорошо обыграли? :)

Умопомрачительно. Если бы не знал, подумал бы, что это распечатки текстов
какой-нибудь компьютерной системы проверки доказательств. Для непосвящённого
выглядит очень похоже. И это в начале 20 века!
По сравнению с RW книжки Ландау являются
образцом краткого и ясного словесного изображения математической мысли.

До этого мне казалось, что наибольшим безумием была конструкция и полное
доказательство правильности универсального алгоритма для машины
Маркова, реализованного на машине Маркова самим Марковым.

Вы читали мой ответ на ваш пост про поступление в аспирантуру? Меня уже взяли Berkeley и Columbia,
я мог бы при случае рассказать вам много интересного. Если вы, конечно, ещё не поступили куда-нибудь.

С вас бутылка:-)

Ага. У остальных университетов такие результаты: Stanford и Harvard отказали,
Princeton поставил в список на ожидание, MIT, Michigan, и Chicago
ещё не ответили.

Да, формально говоря, это и есть огромный такой листинг output'а какой-то программы, но с живыми вычислителями. Матлогика, конечно, рождалась в жутких муках... Про Маркова я слышал, но мне казалось, что это из области фольклора. Если он это записал - тоже очень сильно получается.

Ваши комментарии по поводу аспирантуры читал, спасибо. Если вы не против, отвечу по e-mail чуть подробнее.

избитое место, но манин в своем учебники по логике тоже настаивает, что важно ввести кодировку Геделя в деталях, и собственно делает это.

Не против. Если посещаете физматклуб, можно поговорить там.

да-да, "нормальные алгорифмы" маркова мне вручил колмогоров за турнир городов 1988 года. там, кстати, самого кода примерно на страничку, прямо как какой-нибудь интерпретатор лиспа на лиспе, только гораздо грязнее. вот доказательство - да.

а вот практически то же самое, что и рассел, только действительно проверенное электроникой:
http://us.metamath.org/mpegif/2p2e4.html
хотя есть сейчас и нормальные системы типа coq, более подходящей выразительной силы. inria совместно с microsoft в 2004 году уместили доказательство теоремы четырех красок в два-три мегабайта coq-кода.

Ну понятно, да, что там не столько код, сколько доказательство того, что он делает то, что делает, жуткая штука.

Про coq и т.п. я наслышан, но эту деятельность, честно говоря, недолюбливаю (помимо того, что ей и не интересуюсь...) Как-то было многословное обсуждение - http://archernikov.livejournal.com/26687.html, 4-я и 5-я ссылки.

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

Ага, в моём реферате по философии науки была сноска про это. :)

Сноска - это хорошо :) Я, честно говоря, не могу определиться со своим отношением к этой громаде: с одной стороны понятно, для чего это делалось (цель, причём, на мой взгляд сама по себе вполне дурацкая), но такими методами... Эти люди, судя по всему, роботы.

Зато её легко проверить компьютером, наверное :-) (вспоминая баталии на эту тему)

Да уж. Я, кстати, уверен, что кто-нибудь уже это сделал. Но главное в том, как мне кажется, что её и породить компьютером тоже достаточно легко.

И главное, что никто и разницы не заметит!

Есть ли человек, который её полностью прочитал? (я так поняла, что она вся примерно такая? или нет?)

Вся, да - там выше в комментарии ссылка есть где она отсканирована и выложена в интернет. Боюсь, что такие люди есть. Для её читателей нужно специальную профессию ввести, по аналогии с "Talmudic reader" - "Principic reader", ну и религию заодно. Или предлагаю тест котьюринга - как роботу доказать, что он робот:
1)Написать "Principia"
2)Прочитать "Principia"

Список можно продолжить...

Второго, наверное, достаточно?

Да, конечно, дастаточно любого из пунктов.

"достаточно"

Про Уайтхеда не знаю, но Рассел точно не робот, а разумный интересный мужик; достаточно прочесть его "Историю западной философии".

Я читал, да, спорная книжка. Видимо, всё-таки не робот, а киборг.

http://marina-p.livejournal.com/85621.html

Впечатляет. Сложно поверить, что это написал тот же человек, который придумал О-нотацию!

О-нотация -- это О(х), о(х)? Я не знала, кто её придумал.

Я как-то до сих пор с ним не сталкивалась, кажется. Сегодня в библиотеке попалась на глаза книжка Бляшке, открыла её на послесловии, заметила этот кусок. Захожу в ЖЖ, а там -- ваша запись!

Я, кстати, наврал немного. Придумал ещё раньше Бахман, а Ландау популяризовал. Собственно, и сам недавно узнал - http://archernikov.livejournal.com/24822.html

Класс! замечательные упрямцы. Столько сил положили, чтобы доказать, что строгие доказательства --- возможны.

Доказали?

Легко заметить, что доказали. :-)

Воспитанный человек всегда предпочтет такое не заметить. Или, хотя бы, сделает вид.

Очень тонкое замечание, мне кажется. А про доказали - скорее доказали не то, что возможны, а то, что нафиг не нужны _такие_ доказательства.

"Затянувшуюся тишину прервал наконец Рассел.
- Мой уважаемый коллега-философ из палаты лордов имел несчастье
родиться системным философом в эпоху, когда системной философии уже быть
не может. Надо смотреть правде в глаза, коллега Поппер! Господин
Фейерабенд - умеренный анархический экстремист в теории познания, а я -
неимперативный антиинтуитивный категориалист аналитического стиля,
наконец, лорд Поппер - автор нескольких любопытных концепций, а так вообще
- несинкатегорематический разогреватель онтологически нейтрализованных
зразов в соусе из Circulus Vindobonensis [венский кружок (лат.) -
объединение философов-неопозитивистов, существовавшее в 1920-1924-е годы].
Из Кружка, в котором Витгенштейн сиял, сиял и наконец перестал. А Кружок с
тех пор висит себе на колышке. Ведь эклектический синкретизм работ
господина Поппера...
- Вы меняете взгляды чаще, чем подштанники! - крикнул обозленный,
прямо-таки выведенный из социостатического равновесия лорд Поппер. - Скажи
мне, лорд Рассел, что осталось у тебя от дивной поры молодой? Три тома
"Principia Mathematica" ["Принципов математики" (лат.)], вымученных за
долгие годы. Так вот: спешу сообщить, что Чанг Вэнь или другой
какой-нибудь Пинг-Понг - не запоминаю я этих китайских имен -
запрограммировал компьютер так, что все доказанное Б.Расселом в его
пресловутых "Принципах" машина доказала за восемь минут со средней
скоростью самоубийцы, который бросился с девяностого этажа на Юпитере,
где, как известно, сила тяжести во столько же раз больше земной, сколько
раз домработница господина Тичи ошиблась в счетах из прачечной в свою
пользу."

Станислав Лем, "Осмотр на месте".

Замечательно, спасибо! Лем, как обычно, про всё уже написал.