avatar

Компьютер вывел математическое доказательство, слишком сложное для человека
Опубликовано в Эксперименты



Двое математиков русского происхождения из Ливерпуля, Алексей Лисица и Борис Конев, придумали интересную дилемму: что будет, если заставить компьютерную программу решить математическую задачу, но решение будет слишком сложным и длинным, чтобы его проверил человек?

Для примера учёные взяли так называемую Проблему несоответствия Эрдеша, сформулированную знаменитым венгерским математиком Полом Эрдешем (Paul Erdős). Задача построена вокруг поиска закономерности в бесконечном списке всего двух чисел «1» и "-1". Проблема возникает в тот момент, когда отсекается бесконечная последовательность, а затем создаётся конечная последовательность с использованием определённой константы. Сумма чисел и называется фигурой несоответствия.

Лисица и Конев ввели условия задачи с константой несоответствия «2» в компьютер со специальным программным обеспечение SAT-solvers («Решатели задач выполнимости булевых формул»), которые предназначены для создания математических доказательств.

Компьютер выдал файл с решением математической проблемы, объём которого превышал на пару гигабайтов объём всей «Википедии». Очевидно, что человеку проверить это решение будет не под силу. И потому учёные задают вопрос всем своим коллегам: готовы ли мы настолько доверять компьютерам, чтобы они самостоятельно решали математические и другие логические задачи?
1

Читайте также

  • Эксперименты
    Просто о сложном — интересно о скучном? Да, бросьте, разве физика — это сложно и скучно? Ребята с канала «Гениально» продолжают...
  • Эксперименты
    Поклонники светящихся лесов Пандоры из «Аватара» могут порадоваться: учёные создали биолюминсцентные растения, которые будут...
  • Эксперименты
    10 лет назад, в одном из покинутых городов пустыни Атакама был найден 15-сантиметровый скелет гуманоида с необычной формой черепа и...

Loading...

0 комментариев

Оставить комментарий