Comments 18
Компьютерная программа написала доказательство, другая компьютерная программа проверила доказательство. Вот это действительно магия )))
Из текста следует, что люди, применили самый что ни на есть распространенный прием и свели решение одной задачи к другой (это очень часто делается, есть много теорем доказывающих приводимость многих задач из класса NP друг к другу и решение одной решает множество приводимых к ней). Конкретно в этом случае свели доказательство гипотезы для 7 измерений к решению самой что ни на есть известной NP-трудной задаче теории графов — поиску клики (полностью связного подграфа). Конкретно в этом случае задача решалась не на произвольном графе, а не специфическом, который получался конкретно в этой ситуации (т.е. решение задачи о поиске клики рамером 128 вершин не масштабируется для графов поизвольного вида, они решили ее для одного конкретного графа, обладающего симметрией, как еще одним условием видимо в достаточно обычном методе «ветвей и границ» при переборе всех подграфов. Вроде бы все.
Итого, никакой магии а вполне обычные приемы:
1. Приведение одной задачи задачи к другой
2. Поиск клики в специальном графе (не общего вида а частном случае)
3. Ниличие конкретно в этом частном случае допоплнительных условий позволивших ограничить дерево поиска (видимо) в решении полностью аналогичном методу «ветвей и границ» который часто применяется для поиска клик в графе.
Наверное самое ценное во всем этом результате — это то, что они свели задачу к одной из известных (поиску клики), наличие дополнительных условий ограничивающих дерево поиска достаточно очевидно а уж размышлизмы о размености пространства поиска (2^39 000) вообще попахивает «журналисты изнасиловали ученого» (для оптимизационных задач глупо указывать эти цифры, там в большинстве случаев речь идет о факториалах или показательных функциях)
Итого, никакой магии а вполне обычные приемы:
1. Приведение одной задачи задачи к другой
2. Поиск клики в специальном графе (не общего вида а частном случае)
3. Ниличие конкретно в этом частном случае допоплнительных условий позволивших ограничить дерево поиска (видимо) в решении полностью аналогичном методу «ветвей и границ» который часто применяется для поиска клик в графе.
Наверное самое ценное во всем этом результате — это то, что они свели задачу к одной из известных (поиску клики), наличие дополнительных условий ограничивающих дерево поиска достаточно очевидно а уж размышлизмы о размености пространства поиска (2^39 000) вообще попахивает «журналисты изнасиловали ученого» (для оптимизационных задач глупо указывать эти цифры, там в большинстве случаев речь идет о факториалах или показательных функциях)
Она утверждает, что если замостить двумерное пространство двумерными квадратными плитками, то хотя две из них должны будут соприкасаться сторонами.
Чуть голову не сломал, пытаясь представить себе как можно что-то замостить квадратами так, чтоб никто ни с кем сторонами не соприкасался.
Потом пошел по ссылке на Гипотезу Келлера и увидел, что там написано другое, то что хотя-бы два квадрата будут соприкасаться одной своей стороной друг с другом полностью, от угла до угла. А другими сторонами уже не обязательно полностью соприкасаться только с одним квадратом, можно сразу с двумя. Например, квадраты в школьной тетрадке в клеточку каждой своей стороной соприкасаются только с одним квадратом от угла до угла. А в кирпичной кладке (хоть кирпичи и не квадратные), вертикальной стороной кирпичи соприкасаются только с одним кирпичом, а горизонтальной стороной чаще всего с двумя кирпичами.
Красивый метод решения интересной задачи! Респект!
Встречал таких плиточников, которые, мостя ванную, умудрялись сделать так, чтобы никакие грани друг с другом ровно не совпадали.
Так вы в трехмерном пространстве смотрите, может оно все ровно выглядит в четырех или пятимерном.
Я когда ремонт у себя делал, столкнулся с неевклидовой геометрией стен и непараллельностью ВСЕХ углов. Думаю, эти компьютеры бы с ума сошли, решая такую задачу )))
У вас в переводе, в части про «Язык логики», неточный перевод условия задачи.
В оригинале:
А в переводе:
Это совершенно разные условия.
В оригинале: (NOT A OR NOT B).
У вас же получается: (NOT A AND NOT B).
В оригинале:
Your other co-planner, with an ax to grind, wants to leave off Avery or Brad or both of them.Your other co-planner, with an ax to grind, wants to leave off Avery or Brad or both of them.
А в переводе:
Другой друг не хочет звать ни Алексея, ни Влада.
Это совершенно разные условия.
В оригинале: (NOT A OR NOT B).
У вас же получается: (NOT A AND NOT B).
в программу, проверяющую формальные доказательства через отслеживание логики аргумента,
Где бы скачать такую программу?
ну например: coq.
В подобных статьях было бы интересно видеть и потенциальное практическое применение доказанной теоремы, хотя бы в самых общих чертах.
Интересная статья, спасибо!
В конце же полную таблицу истинности с помощью преобразований привели к совершенной форме — информатика 9 класс
Компьютер выдал не просто односложный ответ. Он присовокупил к нему длинное доказательство на 200 ГБ, поддерживающее это заключение.
Все, человечеству хана. Скоро построим гипердвигатель, а для описания того, как он работает, комп напишет 2 ТБ формул. И инструкции «как починить, если что-то сломалось» там тоже не будет.
Sign up to leave a comment.
Компьютерный поиск помог разобраться с 90-летней математической задачей