И ещё о доказательности.

[fat_yankey]

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

Comments

[ogn_slon]

> Как бы в насмешку, вскоре появилось третье,
> независимое, доказательство, подтверждающее результаты
> американской команды

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

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

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

Статья, кстати, очень хороша. Один из её авторов, R.J.Lipton, сейчас входит в число наиболее авторитетных исследователей сложности вычислений и алгоритмов (фундаментальная проблема "P=NP" и всё вокруг неё). Он ведет отличнейший блог Gödel's Lost Letter and P=NP (highly recommended).

[fat_yankey]

> Почему "как бы в насмешку"?

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

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

Действительно хороша. Поэтому посоветую - перечитайте. Найдёте искомый рассказ.

[ogn_slon]

Я не нашел. Вы процитируйте просто это место.

[fat_yankey]

Понятно. Пока персты не вложу и всё такое. Ну вот, держите:

[declen]

> при том, что одно из них непременно должно было быть неверно.
Совершенно необязательно. Возможно, что в основе топологии лежит противоречивая система аксиом.
Так что может оказаться, что требования "запретить нахуй блядскую топологию" могут воплотиться в жизнь.

[fat_yankey]

> Возможно, что в основе топологии лежит противоречивая система аксиом.

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

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

[declen]

ничего там не противоречиво

[fat_yankey]

> сама статья на которую ссылается автор блога "политическая" и служит как "аргументация" против строгой формализации программирования.

Вам осталось только добавить "средневековая" и можно уверенно деанономизировать - вы дух покойного Эдсгера Дейкстры.

На самом деле статья не политическая, а философская. И не "против" proof of correctness, а за осмысление. Осмысление того, почему практика доказательства корректности программ не нашла поддержки в программистком сообществе.

> Аргументация левая

Та, что вы проводите - несомненно. Но в статье линия аргументации другая.

[leonid_b]

Совершенно жуткая история. Амбец просто. Такое ощущение, что просто земля разверзлась и мироздание зашаталось.
Я не шучу.

[fat_yankey]

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

[leonid_b]

Ну... В общем, после землетрясения большой город существенно более устойчив к следующему землетрясению. Это да.

[booker48]

Сергей Петрович Новиков (лауреат премии Филдса) писал в статье "Математика на пороге XXI века" о переусложнённости доказательств из-за "строгомании":

За последние годы выявилось много случаев, где решения ряда знаменитых математических проблем топологии, динамических систем, различных ветвей алгебры и анализа, как выяснилось, не проверялись никем очень много лет. Потом оказалось, что доказательство неполно (см. мою статью в томе журнала GAFA 2000, посвященного конференции «Vision in Mathematics - 2000», Tel Aviv, August 1999). При этом отнюдь не во всех случаях пробелы могут сейчас быть устранены. Если никто не читает «знаменитых» работ, то как же обстоит дело со сложными доказательствами в более заурядных работах? Ясно, что их в большинстве просто никто не читает. Я могу понять, что решенные в тот же период проблемы Ферма и четырех красок стоят и длинного доказательства, и их проверят. Но постоянно жить в мире сверхдлинных доказательств, никем не читаемых, просто нелепо. Это - дорога в никуда, нелепый конец программы Гильберта.

[bigdrum]

Я прошу прощения, но как математик - недоучка, замечу, что в топологии новых теорем не так уж и много...

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

Пруфы будут?

[booker48]

Аза что вы просите прощения? Вроде, никто и не утверждал, что в топологии новых теорем так уж много... Много теорем - это, кстати, сколько? И пруфы чего/на что?