Max Home IndustryМы наверняка преодолели шок, связанный с участием компьютеров в математических доказательствах? Кажется, что нет, но в этом случае доказательство занимает файл размером 13 ГБ — больше, чем вся Википедия, так что, возможно, мы перешли черту.
Доказанная теорема связана с давней гипотезой Пола Эрдоша.
Пол Эрдош 1913–1996
Теория несоответствия — это то, насколько возможно распределить что-то равномерно. Это происходит во множестве различных форм и даже связано с криптографией.
Его простейшая форма — та, которую Эрдош представил еще в 1930 году. Дана последовательность чисел, состоящая из -1 или 1, а затем рассмотрим любую конечную последовательность длины n, разделенных d элементами, и сформируем сумму элементов.
Гипотеза Эрдоша о несоответствии говорит о том, что вы можете сделать сумму сколь угодно большой.
Например, учитывая последовательность с довольно очевидным шаблоном:
1, -1, 1,1, -1, -1, 1,1,1 -1, -1, -1, 1,1,1,1, -1, -1, -1, -1 и скоро
затем, начиная с третьего элемента, a 1, с интервалом d = 2 и длиной 6, расхождение составляет 1-1 + 1 + 1-1 + 1 + 1, т.е. 3.
Математически гипотеза состоит в том, что для последовательности xn для любого целого числа C> 0 существует подпоследовательность xd, x2d, x3d, … xkd для некоторого выбора натуральных чисел k и d
Очевидно, что несоответствие подпоследовательности измеряет степень, в которой элементы 1 и -1 распределены неравномерно, и гипотезу можно интерпретировать как утверждающую, что независимо от того, как сильно вы пытаетесь создать последовательность, которая равномерно распределена, вы обречены на неудачу, поскольку всегда быть подпоследовательностями с неравномерным распределением 1 и -1, чтобы дать вам любое несоответствие, которое вы хотите назвать.
Вы также можете присвоить исходной бесконечной серии оценку несоответствия как максимальное несоответствие содержащейся в ней подпоследовательности. В этом случае гипотеза утверждает, что каждая бесконечная последовательность имеет бесконечное несоответствие.
Эту простую гипотезу оказалось очень трудно доказать.
В 1993 году было доказано, что бесконечный ряд не может иметь несоответствие 1. Это было сделано путем демонстрации того, что серия длины 12 всегда имеет подпоследовательность с несоответствием больше 1. Поскольку это верно для любой серии длины 12, она должна быть быть верным для любой бесконечной серии, содержащей любое количество подпоследовательностей длины 12.
Таким образом, теорема доказана для C = 1.
Вы можете видеть, что исчерпывающее перечисление всех возможных последовательностей длиной 12, т. Е. 212 (= 4096), и вычисление несоответствия каждой из них путем перечисления каждой подпоследовательности — большая работа, но возможная — на самом деле работа была завершена вручную!
Проблема получила новый всплеск жизни в рамках проекта Polymath, коллективной математической Wiki, экспериментирующей с идеей «краудсорсинговой» математики. Была написана программа, которая искала последовательности с расхождением 2 и находила одну длиной 1124
Недавний прогресс, который подтолкнул C до 2, стал возможен благодаря умной идее использования решателя SAT. Решатель SAT — это программа, которая при задании логического выражения будет пытаться найти набор истинных или ложных присвоений переменным выражения, которые делают его истинным, то есть находит набор значений, удовлетворяющих уравнению.
Проблема SAT была одной из первых, которые были подтверждены как NP-Complete, но это уже другая история. Причина, по которой использование программы SAT-тестирования — хорошая идея, заключается в том, что со временем они были сильно оптимизированы и способны решать очень большие выражения.
Используемая техника состоит в том, чтобы преобразовать последовательность в логическое выражение, которое выполнимо, если существует последовательность длины L несоответствия C. Итак, все, что нужно было сделать, — это создать формулу для каждого L и C = 2 и позволить SAT решатель попытается найти задание, которое сделало его верным. Все шло хорошо до длины 1160, которая, как было доказано, имеет несоответствие 2, но на длине 1161 SAT вернул результат об отсутствии присвоения. Итак, учитывая, что мы уже знаем, что расхождение должно быть больше 1, а не 2, оно должно быть не менее 3.
Следовательно, теперь мы имеем, что гипотеза верна для C = 2.
Следующим шагом была попытка найти последовательность, для которой несоответствие не равно 3, и поэтому мы увеличиваем границу до 3. К сожалению, поиск достиг длины 13000 с несоответствием 3, и именно здесь испытатель SAT выдохся — пора быть точным.
Проблема в том, что сертификат о неудовлетворенности, доказывающий, что последовательность длиной 1161 не имеет подпоследовательности с расхождением 2, составляет 13 ГБ, а в Википедии в настоящее время сжато всего лишь 10 ГБ. Это явно слишком долго, чтобы человек мог проверить или понять.
Как пишут авторы статьи:
«[это] … вероятно, одно из самых длинных доказательств нетривиального математического результата, когда-либо созданных. Его гигантский размер сопоставим, например, с размером всей Википедии, поэтому можно сомневаться в том, в какой степени это можно принять как доказательство математического утверждения «.
Это имеет значение?
Вероятно, нет — до тех пор, пока другие программы могут проверить результат, а сама программа должна считаться частью доказательства.
Куда дальше?
Вычисления дали некоторые подсказки относительно того, как можно было бы взяться за программу в более человеческом масштабе. Между тем программа все еще работает в случае C = 3.