?

Log in

No account? Create an account
И ещё о доказательности. - Книга бревна [entries|archive|friends|userinfo]
Книга бревна

[ картинки | галерея ]

И ещё о доказательности. [Jul. 20th, 2011|10:17 pm]
Книга бревна
[Tags|]
[dow |12571.91]

Незадолго до 1977 года две независимые команды топологов (американская и японская) аннонсировали результаты касающиеся одной и той же гомотопической группы. Результаты противоречили друг другу, а так как оба доказательства оказались весьма сложными, то было совершенно неочевидно кто же из двоих прокололся. Ставки, однако, были достаточно высоки, чтобы не спускать дело на тормозах, и обе команды обменялись результатами для взаимной проверки. Очевидно, что и у тех и у других имелась достаточно сильная мотивация чтобы найти ошибку в доказательстве "соперников", однако же из этого ничего не вышло. Ни американское ни японское доказательство так и не удалось опровергнуть; при том, что одно из них непременно должно было быть неверно.

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

Эта история была рассказана в статье Social processes and proofs of theorems and programs, by Richard A. DeMillo, Richard J. Lipton, Alan J. Perlis; Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977. Статья (не история) наделала много шума и дала начало т.н. Proof of Correctness Wars. К сожалению, авторы из этических соображений не называют никаких имён и фактов, поэтому независимо проверить эту историю у меня не вышло.

На момент выхода этой статьи в математических журналах мира публиковались доказательства примерно 200,000 теорем в год.

Чтение по теме:http://elementy.ru/lib/431269?context=5085665
LinkReply

Comments:
[User Picture]From: monetam
2011-07-21 02:56 am (UTC)
И что ж, ни в одной из версий до сих пор не нашли "прокола" ?
(Reply) (Thread)
[User Picture]From: fat_yankey
2011-07-21 10:33 am (UTC)
Увы, не знаю. Как я уже упомянул, авторы никаих зацепок не дают, отследить историю у меня не получилось.
(Reply) (Parent) (Thread)
[User Picture]From: agasfer
2011-07-21 03:16 am (UTC)
Я думал, вы до октября под парусом прошляетесь.
(Reply) (Thread)
[User Picture]From: bey
2011-07-21 03:47 am (UTC)
ох, одна твердыня была, математика...
(Reply) (Thread)
[User Picture]From: vir77
2011-07-21 03:56 am (UTC)
200 тыщь теорем в год?! Это не опечатка?

Урежьте осетра хотя бы на три нулика
(Reply) (Thread)
[User Picture]From: fat_yankey
2011-07-21 10:31 am (UTC)
Ну, как вы понимаете, я сам не считал. Сколько было в источнике нулей, столько и воспроизвёл. Сомнениями же по поводу размеров осетра вам следует поделиться с паном Станиславом Уламом.
(Reply) (Parent) (Thread)
[User Picture]From: potan
2011-07-21 07:42 am (UTC)
Может таки актиоматика противоречива? :-)
(Reply) (Thread)
[User Picture]From: ogn_slon
2011-07-21 07:46 am (UTC)
> Как бы в насмешку, вскоре появилось третье,
> независимое, доказательство, подтверждающее результаты
> американской команды

Почему "как бы в насмешку"? Просто исследования продолжались.

> Рассказывают, что один из американцев после этой истории
> оставил занятия математикой

Кто рассказывает? В статье ДеМилло и др. этого рассказа нет.

Статья, кстати, очень хороша. Один из её авторов, R.J.Lipton, сейчас входит в число наиболее авторитетных исследователей сложности вычислений и алгоритмов (фундаментальная проблема "P=NP" и всё вокруг неё). Он ведет отличнейший блог Gödel's Lost Letter and P=NP (highly recommended).
(Reply) (Thread)
[User Picture]From: fat_yankey
2011-07-21 10:38 am (UTC)
> Почему "как бы в насмешку"?

Это скрытая цитата. Но вот курьез: он начисто разрушил все пять доказательств, а затем, как бы в насмешку над самим собою, соорудил собственное шестое доказательство!

> Кто рассказывает? В статье ДеМилло и др. этого рассказа нет. Статья, кстати, очень хороша.

Действительно хороша. Поэтому посоветую - перечитайте. Найдёте искомый рассказ.
(Reply) (Parent) (Thread) (Expand)
(no subject) - (Anonymous) Expand
[User Picture]From: declen
2011-07-21 10:48 am (UTC)
> при том, что одно из них непременно должно было быть неверно.
Совершенно необязательно. Возможно, что в основе топологии лежит противоречивая система аксиом.
Так что может оказаться, что требования "запретить нахуй блядскую топологию" могут воплотиться в жизнь.
(Reply) (Thread)
[User Picture]From: fat_yankey
2011-07-21 11:21 am (UTC)
> Возможно, что в основе топологии лежит противоречивая система аксиом.

Возможно, конечно. Вон коллега potan выше то же самое заметил. Но обычно противоречивость системы манифестирует себя более явно. Не прячется за десятками страниц мутных выкладок.

ДеМилло сотоварищи представляли статью в кругу коллег по цеху, поэтому и никаких имён - все и так знали о какой истории речь. И видимо всем было достаточно очевидно, что дело тут не в возможной противоречивости системы аксиом.
(Reply) (Parent) (Thread)
(no subject) - (Anonymous) Expand
(no subject) - (Anonymous) Expand
[User Picture]From: leonid_b
2011-07-21 10:51 am (UTC)
Совершенно жуткая история. Амбец просто. Такое ощущение, что просто земля разверзлась и мироздание зашаталось.
Я не шучу.
(Reply) (Thread)
[User Picture]From: fat_yankey
2011-07-21 11:06 am (UTC)
Ну это ж хорошо. Вибрации мироздания помогают ему утрястись в более устойчивую конструкцию.
(Reply) (Parent) (Thread) (Expand)
[User Picture]From: booker48
2011-07-21 07:06 pm (UTC)
Сергей Петрович Новиков (лауреат премии Филдса) писал в статье "Математика на пороге XXI века" о переусложнённости доказательств из-за "строгомании":

За последние годы выявилось много случаев, где решения ряда знаменитых математических проблем топологии, динамических систем, различных ветвей алгебры и анализа, как выяснилось, не проверялись никем очень много лет. Потом оказалось, что доказательство неполно (см. мою статью в томе журнала GAFA 2000, посвященного конференции «Vision in Mathematics - 2000», Tel Aviv, August 1999). При этом отнюдь не во всех случаях пробелы могут сейчас быть устранены. Если никто не читает «знаменитых» работ, то как же обстоит дело со сложными доказательствами в более заурядных работах? Ясно, что их в большинстве просто никто не читает. Я могу понять, что решенные в тот же период проблемы Ферма и четырех красок стоят и длинного доказательства, и их проверят. Но постоянно жить в мире сверхдлинных доказательств, никем не читаемых, просто нелепо. Это - дорога в никуда, нелепый конец программы Гильберта.
(Reply) (Thread)
[User Picture]From: bigdrum
2011-07-21 09:04 pm (UTC)
Я прошу прощения, но как математик - недоучка, замечу, что в топологии новых теорем не так уж и много...

СПЕЦИФИКА...

Пруфы будут?

(Reply) (Thread)
[User Picture]From: booker48
2011-07-22 04:10 am (UTC)
Аза что вы просите прощения? Вроде, никто и не утверждал, что в топологии новых теорем так уж много... Много теорем - это, кстати, сколько? И пруфы чего/на что?
(Reply) (Parent) (Thread)