Нижняя граница длины доказательства ВТФ

[wd40]

Чтобы поставить точку в спорах о том, мог ли Ферма доказать ВТФ, предлагается доказать новую теорему:

Все знания, известные во времена Ферма, принимаются за аксиомы. В таком случае текст доказательства ВТФ может быть записан не менее, чем $\mathfrak{Y}$ битами.

Можете ли вы доказать хоть какую-нибудь оценку числа $\mathfrak{Y}$?

[Лукомор]

wd40 в сообщении #1198985 писал(а):

Все знания, известные во времена Ферма, принимаются за аксиомы. В таком случае текст доказательства ВТФ может быть записан не менее, чем...

Возможны также другие формулировки, например:
"Все знания, известные во времена Ферма, принимаются за аксиомы.
В такой аксиоматике утверждение, известное как ВТФ невозможно ни доказать, ни опровергнуть".
(Теорема о неполноте знаний в XVII веке).

[arseniiv]

В таком случае можно смело доопределить $\mathfrak Y = \infty$.

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

[wd40]

Лукомор в сообщении #1199002 писал(а):

Теорема о неполноте знаний в XVII веке

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

-- 11.03.2017, 16:42 --

arseniiv
Вообще с абсолютной формализацией в математике есть проблемы. Вот есть ли такая формулировка матана - с аксиомами и правилами вывода?

[arseniiv]

wd40 в сообщении #1199092 писал(а):

Вот есть ли такая формулировка матана - с аксиомами и правилами вывода?

Ну вот Metamath гляньте, там большой кусок этого присутствует.

wd40 в сообщении #1199092 писал(а):

Вообще с абсолютной формализацией в математике есть проблемы.

Да нету проблем. Есть совершенно тривиальная и не новая для множества видов деятельности нехватка рук, мотивированных этим заниматься. Убедите людей — формализуют вам сколь угодно много. Только убедите, всего-то. Чем сильнее и большее число людей, тем меньше придётся ждать.

[Лукомор]

wd40 в сообщении #1199092 писал(а):

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

Письмо весом три тонны в 1847 году почта не приняла бы...

Цитата:

"Наконец, 24 мая [1847 года] было сделано заявление, которое положило конец всем домыслам.
К [Французской] Академии [Наук] обратился не Коши и не Ламе, а Жозеф Лиувилль.
Он поверг достопочтенную аудиторию в шок, зачитав письмо от немецкого математика Эрнста Куммера.
...
Куммер показал, что полное доказательство Великой теоремы Ферма лежало за пределами возможностей существовавших математических подходов. Это был блестящий образец логики и в то же время чудовищный удар по целому поколению математиков, питавших надежду, что именно им удастся решить самую трудную в мире математическую проблему."

Саймон Сингх "Великая Терема Ферма" изд. МЦНМО 2000 г. глава 3 (стр.111-121)

[wd40]

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

Metamath

Цитата:

The complete proof of 2 + 2 = 4 involves 2,863 subtheorems including the 180 above.

-- 11.03.2017, 19:04 --

Лукомор в сообщении #1199119 писал(а):

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

А что такое существующий подход?
Оставим в покое Ферма и поговорим о Гауссе.
Пользовался ли Гаусс только существующими подходами в своей работе? А если нет, имеют ли его открытия право на существование?

[arseniiv]

(Оффтоп)

wd40
К чему была цитата? Вам не нравится формализация? Так вы уж определитесь, нужна она вам или нет, а если вам нужна какая-то особенная, неплохо было бы поделиться соображениями, какая именно.

[wd40]

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

wd40
К чему была цитата? Вам не нравится формализация? Так вы уж определитесь, нужна она вам или нет, а если вам нужна какая-то особенная, неплохо было бы поделиться соображениями, какая именно.

Может поручить компу работу математиков? Какие проблемы? Программистов не хватает? Может комп что-нибудь поинтереснее ВТФ выведет.

[Лукомор]

wd40 в сообщении #1199145 писал(а):

А что такое существующий подход?

Не знаю.
Это не ко мне вопрос, а к Саймону Сингху, которого я цитировал.
Но, IMHO:
во-первых, в приведенной цитате - не "существующий подход", а "существовавшие [на момент написания письма Эрнстом Куммером] математические подходы", что,
во-вторых, мне представляется эквивалентным вашему "Все знания, известные во времена Ферма", с тем только различием, что,
в-третьих,"времена Куммера" отстоят от "времен Ферма" на двести лет бурного развития математики (а от "времен Уайлза" всего на сотню лет!).

Исходя из перечисленного выше,
и, если Куммер прав в том, что для доказательства ВТФ не достаточно было "всех знаний известных во времена Куммера"(средина 19 века),
можно заключить, что для доказательства ВТФ не достаточно было и "всех знаний, известных во времена Ферма (средина 17 века)".

(Оффтоп)

Таким образом, лукоморова "Теорема о неполноте знаний в XVII веке" - доказана!

[Sender]

wd40 в сообщении #1199165 писал(а):

Может комп что-нибудь поинтереснее ВТФ выведет.

А как определить интересность, чтобы даже комп понял?

[mustitz]

wd40 в сообщении #1199092 писал(а):

Лукомор в сообщении #1199002 писал(а):

Теорема о неполноте знаний в XVII веке

Доказать то можно, ведь доказали же.

Доказали в немного другой аксиоматической теории. Всё-таки во времена Ферма знания укладывались скорее в аксиоматику Пеано, из которой не выводиться теория множеств.

[arseniiv]

wd40 в сообщении #1199165 писал(а):

Может поручить компу работу математиков? Какие проблемы? Программистов не хватает?

Программистов, могущих при этом поставить саму задачу. Нельзя сказать компьютеру «сделай как я хочу», надо описать, что именно хочется, и как это оптимальнее сделать.

wd40 в сообщении #1199165 писал(а):

Может комп что-нибудь поинтереснее ВТФ выведет.

Формализация уже имеющегося и вывод нового — это две ортогональные задачи.

[Lia]

Тема перемещена из форума «Великая теорема Ферма» в форум «Карантин»
по следующим причинам:

wd40 в сообщении #1199165 писал(а):

Может поручить компу работу математиков? Какие проблемы?

- отсутствуют собственные содержательные попытки решения задач(и). И этой, и исходной.

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