Доказательства найдены на компьютере

11

В 1996 году давно открытая проблема была решена с помощью компьютера; а именно, что алгебра Роббинса и булева алгебра совпадают. Доказательство было найдено автоматическим испытателем теорем.

Кроме того, известное доказательство теоремы о четырех цветах содержит сгенерированные компьютером компоненты.

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

soft-question big-list proofs automated-theorem-proving Махди Черагчи
источник
2
Некоторые спорадические конечные простые группы (например, группа Лайонсона были впервые построены с использованием компьютера, т. Е. Их доказательство существования (частично) было сгенерировано компьютером)
jp
С этим связан вопрос «Теория сложности эксперимента», используемая для решения открытых задач .
adrianN
ИМХО нужно более тщательно различать «найдено» и «проверено». Gonthier et al. Доказательства определенно не были найдены компьютером.
Gallais
1
Хороший вопрос, но, увы, почти эквивалентен тому, где и как компьютеры помогли доказать это
vzn
Также очень похоже: был ли ранее неизвестный результат доказан автоматическим испытателем теорем? ,
Петр Пудлак

Ответы:

12

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

Из Википедии :

В августе 1998 года Хейлз объявил, что доказательство было полным. На этом этапе он состоял из 250 страниц заметок и 3 гигабайт компьютерных программ, данных и результатов.

Гек Беннетт
источник
10

Это скорее мета-ответ в том смысле, что это список списков.

  1. Бумаги Дорон Цейлбергер . Он математик, и его компьютер указан у соавтора Шалоша Б. Эхада на всех работах, где компьютер играл роль в получении результатов.

  2. Работа Жоржа Гонтье . Он разработал проверенное машиной доказательство теоремы о четырех цветах и ​​недавно работал над теоремой Фейт-Томпсона. Недавно он завершил формализацию теоремы нечетного порядка.

  3. Архив формальных доказательств содержит доказательства, проверенные Изабель, и включает в себя теоремы корректности для алгоритмов, теорему Гаусса-Джордана, некоторую теорию порядка, теорию категорий и многие другие классические результаты.

  4. Формализуя 100 теорем , содержит проверенные машиной доказательства некоторых известных теорем.

Виджай Д
источник
1
Спасибо. Я должен уточнить, что мой вопрос не касается доказательств, проверенных / подтвержденных компьютерами после обнаружения, а также результатов, когда компьютер сыграл свою роль в их получении (конечно, мы все используем компьютеры в наших исследованиях, но в конечном итоге получаем автономные математические данные). доказательство того, что мы не можем сказать, было «получено» компьютером). Я ищу предположения, доказательства которых были сгенерированы (полностью или частично) компьютером.
Махди Черагчи