Самое длинное доказательство

[e7e5]

Возник такой вопросик, наверное очень простой:
А какое существует самое длинное и самое короткое доказательство в математике на сегодняшний день?

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

[Someone]

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

На программу проверки доказательств где-то была ссылка (кажется, в теме Котофеича о противоречивости ZFC).

[sceptic]

Проект "доказатель теорем" Coq. Разработан во Франции. Подробнее о Coq.

[Mopnex]

А ещё есть доказательство теоремы о 4-х красках. Там вроде бы даже никто не пытался его выписать, слишком много.

[Nilenbert]

Насчёт самого короткого доказательства - смотрите у Литтлвуда в "Математической смеси" про доказательства в одну строку, там приводятся примеры(доказательства бесконечности числа простых чисел, основной теоремы алгебры и т.д.)

[Schraube]

Теорема Фейта-Томсона (Всякая нециклическая конечная группа нечетного порядка разрешима)
Опубликовано, кажется, на 800 стр.
Надо поискать ссылки

[AD]

А что там с теоремой Карлесона (ряд фурье функции из $L_2$ сходится почти всюду)? У нас периодически бывает годовой спецкурс про нее одну. Хотя, вообще, да, на 800 страниц не тянет всё равно.

Или там просто слишком много вспомогательной инфы? Вообще, как мы отделяем леммы от собственно теоремы, и леммы, относящиеся к теореме, от лемм, не относящихся?

_________________

Mopnex в сообщении #208960 писал(а):

А ещё есть доказательство теоремы о 4-х красках.

Где-то слышал, что уже нашли человеческое доказательство, и даже алоритм закраски. Это правда?

[Юстас]

Кстати, вроде есть альтернативное более короткое доказательство теоремы Карлесона, автор - Michael Lacey.

[tolstopuz]

Mopnex писал(а):

А ещё есть доказательство теоремы о 4-х красках. Там вроде бы даже никто не пытался его выписать, слишком много.

Доказательство на языке Coq занимает мегабайта три.

Schraube писал(а):

Теорема Фейта-Томсона (Всякая нециклическая конечная группа нечетного порядка разрешима)
Опубликовано, кажется, на 800 стр.

255. Теперь фактически является частью классификации конечных простых групп, о которой говорил Someone.

[Schraube]

tolstopuz писал(а):

255. Теперь фактически является частью классификации конечных простых групп, о которой говорил Someone.

Приветствую. Это Михалыч, которого не регистрируют под девичьей фамилией
Да. Вы правы. Кажется, говорится у Конвея и Слоэна.
Но о первом доказательтве говорили в пору моей молодости как о рекордном по длине.

[Ktina]

Пожалуйста, не убивайте меня за некропостинг!
http://hijos.ru/2014/02/26/matematiches ... -proverit/

[grizzly]

(Оффтоп)

Ktina в сообщении #1072153 писал(а):

Пожалуйста, не убивайте меня за некропостинг!

Содержание статьи принципиально устарело. Недавно Теренс Тао доказал эту гипотезу. Здесь уже было.

Про автоматизированные проверки доказательств за эти годы было много полезной информации на вполне популярном уровне. Помню интересную лекцию Матиясевича на эту тему. У Вавилова тоже была хорошая лекция про вопросы, связанные с доказательствами. Я давал раньше здесь ссылки на эти лекции -- наверняка обе легко гуглятся.

[tolstopuz]

tolstopuz в сообщении #209034 писал(а):

Schraube писал(а):

Теорема Фейта-Томсона (Всякая нециклическая конечная группа нечетного порядка разрешима)
Опубликовано, кажется, на 800 стр.

255. Теперь фактически является частью классификации конечных простых групп, о которой говорил Someone.

За прошедшие годы и его перевели на Coq. 7 мегабайт.

[Anton_Peplov]

tolstopuz в сообщении #1072234 писал(а):

За прошедшие годы и его перевели на Coq.

Перевели доказательство теоремы Фейта-Томсона или все теоремы о классификации конечных простых групп?

[Xaositect]

Фейта-Томпсона. http://ssr2.msr-inria.inria.fr/~jenkins ... gress.html