Гипотеза Римана

[Sender]

Munin в сообщении #1341594 писал(а):

А если ошибочно введена формулировка теоремы, которую надо доказать?

Всё-таки формулировка обычно достаточно коротка, чтобы правильность её ввода можно было без особых усилий проверить вручную.

[arseniiv]

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

[Munin]

Sender в сообщении #1341597 писал(а):

Всё-таки формулировка обычно достаточно коротка

Это когда введены все используемые в ней понятия. А если спускаться на элементарный уровень, увы, нет.

[Sender]

Red_Herring в сообщении #1341573 писал(а):

А она существует для задач анализа?

Вот, к примеру, в metamath есть список из 100 известных теорем, которые предполагается доказать в этой системе, чтобы сравнить её эффективность с другими аналогичными системами. Среди доказанных можно встретить, к примеру, такие вещи, как основная теорема интегрального исчисления, несчётность континуума, расходимость гармонического ряда, теорема Кантора о мощности булеана и т.д.
http://us.metamath.org/mm_100.html

arseniiv в сообщении #1341600 писал(а):

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

Они обычно используются также для множества других теорем, ранее уже записанных в используемой системе. Вряд ли каждая следующая теорема привносит такое уж значительное их количество. Но, пожалуй, да, это может оказаться слабым местом - мы доказываем совсем не то, что хотим. Какие приёмы для борьбы с этим используются в обычных доказательствах?

[Rak so dna]

Sender в сообщении #1341605 писал(а):

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

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

[mihaild]

Rak so dna в сообщении #1341610 писал(а):

поэтому возвращаемся к этим нашим формализованным определениям и разбираемся что же они означают на самом деле

Процесс разбирательства существенно неформальный.

Rak so dna в сообщении #1341610 писал(а):

На верность имеющегося доказательства это не влияет

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

[Rak so dna]

mihaild в сообщении #1341617 писал(а):

Процесс разбирательства существенно неформальный.

Согласен, но это не влияет на верность доказательства. Это лишь наше понимание того, что мы там наопределяли.

mihaild в сообщении #1341617 писал(а):

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

Процесс формализации утверждения является частью проверки всего доказательства, иначе нет смысла строить такие системы.

[Skipper]

Red_Herring в сообщении #1341459 писал(а):

И истину можно прекрасно установить и без того, чтобы о ней сообщать в интернет..

Вот я и хочу установить истину.
Как и многие другие- хотят узнать - ответ на вопрос "доказал ли Атья гипотезу Римана, али не доказал" ?

А тут вместо того чтобы дать этот ответ, начинают придираться к смыслу слов "официально признали" ,
(что доказательство верное) или не признали официально.. И т.д. и т.п.

А большинство людей (>99%) просто не захотят в эти все тонкости вдаваться.
Потому я и привёл пример с Перельманом - как один из показателей. Раз уже ему предлагали премию в 1 млн долларов,
значит точно он ту гипотезу доказал. Вот это обществу понятно.

Заявят "великие математики", что ГР доказана, и позовут чтобы вручить Абелевскую премию за доказательство -
тогда обществу будет понятно, что "официально" признано, что и это доказано.

И в доказательстве на 5 страниц, все эти проверки , должно быть, можно сделать достаточно быстро.

[arseniiv]

Sender в сообщении #1341605 писал(а):

Какие приёмы для борьбы с этим используются в обычных доказательствах?

Как понимаю, те же (почти никакие), что и в формализованных, просто проверявших в первом случае сильно больше.

Rak so dna в сообщении #1341626 писал(а):

Процесс формализации утверждения является частью проверки всего доказательства, иначе нет смысла строить такие системы.

Если вероятности ошибиться уменьшаются — есть. Но они не уменьшаются до нуля. Ошибки обоих родов остаются возможными, это и хотели вам сказать.

[a1981]

Skipper, Вам намекнули на ответ...И объяснили, почему не хотят говорить прямо...

[mihaild]

Rak so dna в сообщении #1341626 писал(а):

Процесс формализации утверждения является частью проверки всего доказательства, иначе нет смысла строить такие системы.

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

[Dmitriy40]

Мне, хоть и далёкому от математики, тоже интересно доказал или нет. И ситуация с нахождением ошибок, но скрытия этого факта от СМИ мне не нравится, даже по непонятным моральным мотивам.
Другое дело если не опровергают публично давая возможность поправить самому автору. Тут я готов подождать месяцы (для настолько короткого доказательства) пока и перепроверят десяток математиков с мировым именем (вот не буду детализировать, обывателю и так понятно кто это), и доведут до ума если оно всё же имеет легко устранимые огрехи.

Критерий цитируемости как верности доказательств как минимум странный (чтобы не сказать сильнее): это что, если перестанут цитировать теорему Пифагора -- она перестанет быть верной?!

[a1981]

С учетом того, что понаписали СМИ, главной ошибкой было донесение до них этой истории

[Munin]

Skipper в сообщении #1341629 писал(а):

Вот я и хочу установить истину.
Как и многие другие- хотят узнать - ответ на вопрос "доказал ли Атья гипотезу Римана, али не доказал" ?

А тут вместо того чтобы дать этот ответ, начинают придираться к смыслу слов "официально признали"

У вас распространённая проблема: хотите узнать одно, а спрашиваете другое.

Истину, к сожалению, установить невозможно. (Многие сомневаются, что она вообще есть.) Максимум - можно произнести какие-нибудь успокаивающие слова для публики, с важным видом.

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

[Rak so dna]

удалил