Математические теоремы на компьютере

[Icarus]

Мне вот стало интересно, а если какие-нибудь математические теоремы, которые проверялись на компьютере ну для очень больших $n$ и все было cool, а потом доказали, что теорема неверна. Ну, для примера, возьмем гипотезу Лежандра о том, что для любого $n$, между $n^2$ и $(n+1)^2$ всегда найдется просто число. И вот мы проверяем-проверяем на компьютере, и действительно находятся, а в один день доказали бы, что это выполнятся не будет. Возможно, не очень удачный пример, но надеюсь понятно, что я имел ввиду. Вообщем, были ли такие истории?

[demolishka]

Величина $\pi(x) - \operatorname{Li}(x)$ меняет знак бесконечное число раз, хотя рассмотрение соответствующих графиков предсказывает совершенно обратное (см. тут). Хоть эта теорема была доказана задолго до появления компьютеров, но все же говорит про компьютерную интуицию и реальное положение дел в теоретико-числовых вопросах.

[Sonic86]

https://nplus1.ru/material/2015/08/21/a ... nd-corners
Вот интересная история об открытии замощении плоскости пятиугольниками.

Icarus в сообщении #1420419 писал(а):

а потом доказали, что теорема неверна.

Правильно говорить так: обнаружили, что доказательство содержит ошибку. Доказать, что какая-либо теорема неверна, в принципе невозможно.

[Icarus]

Sonic86 в сообщении #1420462 писал(а):

Вот интересная история об открытии замощении плоскости пятиугольниками.

Интересно, конечно, но по сабжу ничего там не нашел. Да, перебором на компьютере нашил новое замощение.

Sonic86 в сообщении #1420462 писал(а):

Доказать, что какая-либо теорема неверна, в принципе невозможно.

Под "теорема неверна" я имел ввиду, что доказали отрицание к теореме.

demolishka в сообщении #1420423 писал(а):

Величина $\pi(x) - \operatorname{Li}(x)$ меняет знак бесконечное число раз, хотя рассмотрение соответствующих графиков предсказывает совершенно обратное (см. тут).

Это уже практически то, что я хотел, спасибо.

[mihaild]

Icarus в сообщении #1420471 писал(а):

Под "теорема неверна" я имел ввиду, что доказали отрицание к теореме

Просто теорема - это то, для чего есть доказательство. Если нашли контрпример - то значит доказательства нет и не было. Ну либо теория противоречива, но такого пока в крупных разделах не происходило.
В обсуждении на math.se есть подборка гипотез, к которым наименьший контрпример большой. Например $n^{17}+9$ и $(n+1)^{17} + 9$ взаимно просты при $n < N$ и не взаимно просты при $n = N$, где $N \approx 8.4 \cdot 10^{52}$.

[Sonic86]

Icarus в сообщении #1420471 писал(а):

Это уже практически то, что я хотел, спасибо.

Значит скорее всего Вас интересуют не теоремы, а гипотезы. Их можно просто нагуглить.

[Icarus]

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

Просто теорема - это то, для чего есть доказательство.

Хм, то есть теорему Ферма до 1995 года называли гипотезой Ферма или проблемой Ферма?

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

В обсуждении
на math.se есть подборка гипотез, к которым наименьший контрпример большой. Например $n^{17}+9$ и $(n+1)^17 + 9$ взаимно просты при $n < N$ и не взаимно просты при $n = N$, где $N \approx 8.4 \cdot 10^{52}$.

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

Я кажется фигово объяснил что хотел. Представим параллельную вселенную. В этой параллельной вселенной есть Ферма (раз уж вспомнил про него), который делает свое знаменитое утверждение. Все тщетно бьются над доказательством или опровержением. Наступает середина ХХ века. Ищем контрпример на компьютере. Очень большие $n$, но ничего не получается. И вот наступает 1995, появляется параллельный Эндрю Уайлс, который каким-то там образом показывает, что такой контрпример должен существовать. Вот. Я хочу узнать были ли похожие истории в нашем мире.

-- 13.10.2019, 18:38 --

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

В обсуждении
на math.se есть подборка гипотез, к которым наименьший контрпример большой.

Хотя не, это было бы прям то, что мне нужно, если бы там не находили контрпример, а доказывали, что он должен быть. Может я в этом месте туплю? Показать, что контрпример есть $=$ найти этот контрпример? Ну как бы да, но всегда ли?

[mihaild]

Icarus в сообщении #1420494 писал(а):

Хм, то есть теорему Ферма до 1995 года называли гипотезой Ферма или проблемой Ферма?

Нет, но это историческое наименование. До 1995 года не было известно, является ли "теорема Ферма" теоремой

Icarus в сообщении #1420494 писал(а):

если бы там не находили контрпример, а доказывали, что он должен быть

Т.е. вы хотите чистое доказательство существования, без оценок? Это должен быть какой-то очень специальный метод доказательства, чтобы из него нельзя было вытащить вообще никакую верхнюю оценку.
Либо можно придумать специальную проблему для этого. Например, пусть $f(n)$ - максимальное число колмогоровской сложности меньше $n$. Тогда $f(n)$ очевидно стремится к бесконечности, но не существует алгоритма, вычисляющего верхнюю оценку на $f(n)$ (если бы такой алгоритм существовал и вычислял функцию $g(n)$, то $g(n) + 1$ имело бы сложность хотя бы $n$, а находить сложные слова алгоритмически невозможно).

[Icarus]

mihaild
Еще раз просмотрел ссылку, пожалуй, то что нужно, спасибо.
Под "доказывали, что он должен быть" я имел ввиду, что этот контрпример ручками бы как-то находился, а они там все через компьютер. Так что доказательства с оценками очень даже мне подходят.

[Munin]

Sonic86 в сообщении #1420462 писал(а):

Доказать, что какая-либо теорема неверна, в принципе невозможно.

Возможно, если мы эту теорему рассматриваем в приложении для разных объектов, или например, в разных аксиоматиках. Например, для каких-то колец "основная теорема арифметики" верна, а для каких-то - неверна. В аксиоматике Евклида (на евклидовой плоскости) теорема Пифагора верна, а в аксиоматике Лобачевского (на плоскости Лобачевского) - неверна.

Icarus в сообщении #1420471 писал(а):

Под "теорема неверна" я имел ввиду, что доказали отрицание к теореме.

Отсутствие доказательства не всегда подразумевает, что существует доказательство обратного. Существуют факты, которые верны, но недоказуемы (и тогда теоремы нет, поскольку теорема подразумевает доказательство).

[Icarus]

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

Существуют факты, которые верны, но недоказуемы

Можно пример? (надеюсь Вы не про аксиомы сейчас)

[mihaild]

Icarus в сообщении #1420544 писал(а):

Можно пример? (надеюсь Вы не про аксиомы сейчас)

Аксиомы как раз доказуемы (и даже в одну строчку).
Формулировка "существуют верные недоказуемые утверждения" - стандартная неточная переформулировка утверждения "арифметика неполна" (или какая-то другая теория - почти все интересные встречающиеся на практике теории неполны). Например, в ZF все можно доказать, что все последовательности Гудстейна конечны. А в арифметике это утверждение всё еще можно сформулировать, но уже нельзя доказать.
Правда почему в такой ситуации надо называть это утверждение "истинным, но не доказуемым" - я не понимаю. В ZF оно доказуемо, а без ZF непонятно, почему нужно считать это утверждение истинным.

[Icarus]

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

А в арифметике это утверждение всё еще можно сформулировать, но уже нельзя доказать.

А как доказывают, что нельзя доказать?

[mihaild]

Icarus в сообщении #1420563 писал(а):

А как доказывают, что нельзя доказать?

По-разному. Например берут какую-то более мощную теорию (например ZF) и в ней строят модель арифметики (т.е. какое-то множество и определение сложения и умножения на нём), в которой выполнены все аксиомы арифметики, но не выполнено наше утверждение.