avatar

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



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

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

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

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

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

  • Эксперименты
    На этот раз доступно и понятно ребята канала «Гениально» расскажут про теплоту, точнее три теплоты.
  • Эксперименты
    Компания KMel Robotics создаёт удивительные квадрокоптеры, которые по одиночке мало кому покажутся интересными. Зато, объединённые в...
  • Эксперименты
    Откуда есть пошла Земля Русская… Нет, это слишком мелко и этим пусть историки занимаются. Откуда есть пошла Вселенная — вот это наш...

Loading...

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

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