Где и как компьютеры помогли доказать теорему?

55

Цель этого вопроса - собрать примеры из теоретической информатики, где систематическое использование компьютеров было полезным

  1. в построении гипотезы, которая приводит к теореме,
  2. фальсификация гипотезы или доказательного подхода,
  3. построение / проверка (части) доказательства.

Если у вас есть конкретный пример, пожалуйста, опишите, как это было сделано. Возможно, это поможет другим более эффективно использовать компьютеры в своих ежедневных исследованиях (что на сегодняшний день все еще кажется довольно редкой практикой в ​​TCS).

(Помечено как вики сообщества, поскольку нет единого «правильного» ответа.)

Moritz
источник
Я должен сказать, что я особенно заинтересован в случаях (1) и (2). То есть случаи, когда компьютеры помогали сформировать человеческую интуицию в решающих отношениях.
Мориц
2
Некоторые из последних ответов на этот вопрос, приведенные в конце списка, превосходны и их стоит прочитать. Предлагаю прочитать до конца!
Андрас Саламон

Ответы:

32

Очень известный пример - теорема о четырех цветах , первоначально доказанная исчерпывающей проверкой.

Евгений Торстенсен
источник
6
(Возможно) не теоретическая информатика.
Джефф
20

n

Показывать, что проблема минимальной триангуляции (MWT) была NP-трудной, была давней открытой проблемой, осложненной тем фактом, что длины ребер включают в себя квадратные корни, и желаемую точность, необходимую для их точного вычисления, было трудно определить.

Малзер и Роте показали, что MWT был NP-hard , и в процессе использовали компьютерную помощь, чтобы проверить правильность своих гаджетов. Насколько я знаю, альтернативных доказательств нет.

Суреш Венкат
источник
20

Доказательство Томаса Хейлса (его сайт, MathSciNet ) гипотезы Кеплера включало в себя так много анализа случаев - и случаи в свою очередь проверялись компьютером - что он решил попытаться получить формальное доказательство этого. Его проект для этого - FlysPecK , и он оценивает, что это займет 20 лет работы.

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

Джошуа Грохов
источник
20

Дорон Цайлбергер проделал определенную работу в области компьютерных доказательств. В частности, он подготовил программу Maple для доказательства геометрических тождеств и другую программу для доказательства класса комбинаторных тождеств . Некоторые из методов , которые упоминаются в книге A = B .

Томер Вромен
источник
20

Компьютеры также использовались для определения верхних границ времени выполнения программ обратного отслеживания, решающих сложные задачи NP, и создания гаджетов для подтверждения результатов неприемлемости. Эта и другие веселые темы ждут вас в коротком эссе (предупреждение, предельная самореклама), озаглавленном «Применение практики к теории». Смотрите http://arxiv.org/abs/0811.1305

Учитывая этот хороший список, похоже, я должен обновить статью!

Райан Уильямс
источник
Да, мне это тоже нравится.
Даниэль Апон
18

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

RJK
источник
15

Я не видел здесь упомянутого, но автоматическое средство проверки теорем решило давнюю открытую проблему того, являются ли алгебры Роббинса булевыми:

http://www.cs.unm.edu/~mccune/papers/robbins/

Это особенно примечательно, потому что компьютер разработал все доказательства, и проблема была открыта в течение нескольких десятилетий.

Не совсем уверен, что он квалифицируется как TCS, но, возможно, он тесно связан.

Мугизи Рвебангира
источник
1
Ответ, упоминающий об этом, был размещен в середине августа, но ответ был удален владельцем в конце сентября. Это хороший пример.
Андрас Саламон
14

Алгоритм Карлофф-Цвик для MAX-3sat достигает ожидается , производительность 7/8. Однако анализ основан на недоказанных сферических объемных неравенствах. Это неравенство было окончательно подтверждено с помощью компьютерных доказательств в другой статье Цвика .

Помимо доказательства Хейлса к гипотезе Кеплера, как упомянуто выше, доказательство к гипотезе Сота и к гипотезе Додекаэдра также автоматизировано.

оборота Зейю
источник
1
Пока мы в этом духе, опровержение Вейром и Феланом гипотезы Кельвина было также автоматизировано. ( en.wikipedia.org/wiki/Weaire%E2%80%93Phelan_structure )
Питер Шор
11

Вы можете проверить домашнюю страницу Shalosh B. Ekhad . Этот компьютер некоторое время публиковал статьи (обычно с соавторами).

Лев Рейзин
источник
11

Кристиан Урбан использовал ассистента по доказательству Изабель, чтобы проверить, что одна из основных теорем в его докторской диссертации была фактически теоремой [1]. Используя ассистента, нужно было сделать несколько изменений, но результат в значительной степени выдержал.

Точно так же Урбан и Нарбу также обнаружили ошибки в ручном и бумажном доказательстве доказательства полноты Crary для проверки эквивалентности.

Meikle и Fleuriot формализовали Grundlagen Гильберта в Изабель и продемонстрировали, что, вопреки утверждениям Гильберта, он все еще полагался на свое интуицию, чтобы формализовать геометрию аксиоматическим образом (в его доказательстве были пробелы, полученные от Гильберта, предполагающего что-то о диаграммах) [3] ,

[1]: Пересмотр сокращения выреза: одно трудное доказательство действительно доказательство

[2]: формализация в доказательстве полноты номинальной Изабель Крэри для проверки эквивалентности

[3]: Формализация Грюндлагена Гильберта в Изабель / Изаре

Доминик Маллиган
источник
10

Результаты в « Геометрии деревьев бинарного поиска » Демейна, Хармона, Яконо, Кейна и Патрашку были разработаны с помощью программного обеспечения для тестирования различных схем начисления платы и построения оптимальных оценок для последовательностей с малым доступом. (И да, «ослы» - это правильный термин.)

Jeffε
источник
1
Под "ослами" я предполагаю, что вы имеете в виду "Arborally Satisfied Set"? Может быть, я отдал удовольствие от аббревиатуры. :)
Андрей В.
10

Н. Шанкар проверил (полностью и механически) доказательство Гёделем теоремы неполноты и теоремы Чёрча - Россера, используя доказательство теоремы Бойера - Мура. Есть книга, описывающая, как это было сделано.

Раду ГРИГОРЕ
источник
6

Есть множество примеров в анализе средних случаев алгоритмов. Возможно, некоторые из самых ранних - это компьютерные эксперименты, которые привели к публикации в STOC 1984 «Некоторые неожиданные ожидаемые результаты поведения для упаковки бинов», выполненной Бентли, Джонсоном, Лейтоном, МакГеохом и МакГеохом.

Питер Шор
источник