Как стать автором
Обновить

Комментарии 25

Очень теорему, значит. Ну ладно

Это же явно перевод — почему нет ссылки на оригинал статьи?

Корпоративные блоги видимо не ездят по общим рельсам. На самом деле ссылка в статье на исходник есть, но она не в заголовке.


пишет Nature.
Ну и в какой момент мы скатились до того, что код в статье на хабре является просто абстрактной картинкой-иллюстрацией для привлечения внимания? Ну спасибо хоть не HTML вставили.

Что пытается донести эта статья? Что есть такой раздел математики как топология? Так мы в курсе. Что есть proof assistance? Так мы в курсе. Что кто-то назвал что-то другое революционным? Так нам плевать.

В статье ровно ноль интересной информации.
хабр-бизнес, ничего личного…
В каком-то смысле данная статья демонстрирует степень неэффективности формального кодирования теорем:
По словам одного из помощников Йохана Коммелина, Lean-версия доказательства Шольце включат десятки тысяч строк кода — она примерно в 100 раз больше, чем оригинальная версия

У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.
У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.

Вопрос ещё и в том, сколько ошибок и неточностей в доказательстве при этом было найдено.


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

Естественным образом мы приходим к кризису проверяемости в науке.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?

Более того, даже вне контекста формализованных проверок, в случае математики, мы начинаем наблюдать разделение на школы — японская школа, считающая abc conjecture доказанной, и европейская школа (включая, что иронично, собственно Шольце), отрицающая доказательство Мотидзуки. Иными словами, мы вплотную подошли к моменту, когда доказательство приходится принимать «на веру». Судя по всему, это первые звоночки надвигающегося кризиса.

Резюмируя: мы уже не справляемся с классической проверкой отдельных теорем, а формальное кодирование требует кратно больших усилий. Соответственно, нужно изобретать совершенно новую парадигму для кодирования, поскольку в текущем виде это тупиковый подход.
Вот пруфчекер Globular, где доказательства строятся в виде картинок по принципу «раскрась сам».
golem.ph.utexas.edu/category/2015/12/globular.html
Он для специальной области, не для всего. Придумали, что характерно, посторонние люди (квантовые физики), у которых взгляд не замылен.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?

Только после того, как вы всё закодировали, проверять это доказательство людям не нужно. Вы прогоняете чекер на вашем коде, он вам говорит «норм, молоток», и всё. Доверять нужно не тому десятку математиков, которые осилили прочитать доказательство конкретной теоремы, а только ядру чекера (которое сильно проще, и которое могли прочитать десятки тысяч математиков, так как этот чекер использовался для доказательства ещё 100500 теорем).

Я не совсем корректно выразился: как показывает статья выше, кодирование многократно более времязатратно (предполагая, что вобще осуществимо), чем классическое доказательство, однако, действительно не будет требовать дополнительной "внешней" проверки сообществом.

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

Де-факто проверка сообществом, в данный момент, это единственный способ верификации.

В случае чекера мне тоже не все очевидно: что делать, например, когда создается новая область? Как проверить, что новые понятия и объекты корректно закодированы? Для меня это выглядит так, что все равно потребуется внешняя проверка, но тогда мы возвращаемся к изначальной теме - будет ли в таком случае профит, кроме самого факта кодирования.

Пусть мы закодировали и верифицировали, это позволяет нам доказать Х теорем внутри данной области. Но, во-первых, каждая новая отрасль будет требовать нового кодирования и верификации, во-вторых, мы тратим на это время, причем значительное. Мне не очевидно, что это жизнеспособный способ доказательства.

В случае чекера мне тоже не все очевидно: что делать, например, когда создается новая область?

Записать её в терминах логики, реализуемой чекером.


Как проверить, что новые понятия и объекты корректно закодированы? Для меня это выглядит так, что все равно потребуется внешняя проверка, но тогда мы возвращаемся к изначальной теме — будет ли в таком случае профит, кроме самого факта кодирования.

Да, будет, потому что вы должны проверить только определения тех терминов, с которыми вы работаете, и утверждения теорем.


Для одного куска проекта, над которым я сейчас работаю (формализация некоторого модельного языка программирования и доказательство его свойств), определения — строк 200, утверждения двух ключевых теорем — строк 10, остальной код — тыщ пять. Человеку достаточно прочитать ту первую пару сотен строк, все эти прочие тыщи — они не для него. Собственно, вот определения: синтаксис языка, его система типов, его семантика. Вот утверждения ключевых теорем: раз, два.


Учитывая, что в человекочитаемом виде в статье это всё занимает страницы три-четыре, в итоге получается плюс-минус то же. Да и по внешнему виду тоже: сравните, например, определение системы типов в машинопонятном виде выше с её определением в статье для людей:


тыц


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


тыц


Мне не очевидно, что это жизнеспособный способ доказательства.

А ничего лучше нет. Можно, конечно, ручкой и бумажкой, но надёжность и доверие таким доказательствам падают даже для очень маленьких групп теорем. В чужих статьях, отрецензированных, опубликованных, доложенных на конференциях, и так далее, я ошибки находил.

Записать её в терминах логики, реализуемой чекером.

Это не означает автоматически, что мы корректно закодировали новые понятия и объекты, нам так или иначе нужна внешняя проверка.
Учитывая, что в человекочитаемом виде в статье это всё занимает страницы три-четыре, в итоге получается плюс-минус то же. Да и по внешнему виду тоже: сравните, например, определение системы типов в машинопонятном виде выше с её определением в статье для людей:

Здорово, что такой подход работает в вашей области. Но это не означает, что мы получим аналогичный коэффициент «выгоды» для других областей — в эту пользу говорит не закодированность большей части математики.

А ничего лучше нет. Можно, конечно, ручкой и бумажкой, но надёжность и доверие таким доказательствам падают даже для очень маленьких групп теорем. В чужих статьях, отрецензированных, опубликованных, доложенных на конференциях, и так далее, я ошибки находил.

Поэтому я утверждаю, что нам нужны будут новые инструменты. В данный момент, используя кодирование, мы делаем двойную работу — нужно, условно, Х времени, чтобы понять объект, который мы кодируем, и Х10, чтобы его закодировать.

Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.
Это не означает автоматически, что мы корректно закодировали новые понятия и объекты, нам так или иначе нужна внешняя проверка.

А как вы проверите, что математики правильно проверили, что статья действительно об одной теме, а не о другой?


Но это не означает, что мы получим аналогичный коэффициент «выгоды» для других областей — в эту пользу говорит не закодированность большей части математики.

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


В данный момент, используя кодирование, мы делаем двойную работу — нужно, условно, Х времени, чтобы понять объект, который мы кодируем, и Х10, чтобы его закодировать.

Нет. Просто машина-то тупая, ей не скажешь «очевидно, что…», «предположим, что все переменные имеют разные имена», и так далее. Ей это надо конкретно и детально объяснять, и там уже часто получается, что некоторые вещи и самому перестают быть очевидны.


Не уверен, что всякие нейралинки тут помогут.

Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.
Почему нейроинтерфейс нужен? Они нужны, чтобы продвинуть физику. Вот здесь довольно подробно написал на эту тему. Чтобы продвинуть математические методы, кот. в первую очередь опять же нужны для построения новых физических теорий, нужен продвинутый интеллект, а это только ИИ, возможно в интерфейсе с человеком (симбиотический ИИ), см. комент в той же статье. Вообще коменты в той статье по поводу той же импликации напомнили мне средневековые схоластические споры) вроде приводят логические выводы, но результаты получаются разные.
Де-факто проверка сообществом, в данный момент, это единственный способ верификации.
Как-то сомнительно для меня все это звучит.

В моем понимании, если вы не способны выразить ваше доказательство в какой-либо формальной системе, то лучше считать что у вас нет полного доказательства, а только его набросок. Дальше уже перевести из одной формальной системы в синтаксис proof assistance не выглядит такой уж сложной задачей, плюс, по дороге вы проверите, какие инструменты доказательства вы использовали.

Я охотно допускаю, что даже сотни пар просветленных глаз способны одинаково ошибаться, если у них одна и та же база знаний. Так что все вариации на тему «очевидно что A => B» приниматься на веру не должны, особенно если A и B не вполне определены формально.

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

Так и в математике: если мы доверяем корректной реализации proof assistance, то теорему следует считать доказанной как только мы соглашаемся с аксиоматической базой и допустимыми методами выведения термов.

Боюсь, без формализации современная математика превратится в астрологию, где ваши представления будут основываться на субъективной вере/доверии к авторитету источника утверждения.

Ну и последнее, математическое утверждение корректно или не корректно независимо от того, способны ли вы осмыслить доказательство в силу своих природных ограничений. Потому полагаться в этом вопросе на более надежные вычислители – хорошая идея.
Как-то сомнительно для меня все это звучит.

Может быть, но таково состояние вещей в данный момент.
В моем понимании, если вы не способны выразить ваше доказательство в какой-либо формальной системе, то лучше считать что у вас нет полного доказательства, а только его набросок. Дальше уже перевести из одной формальной системы в синтаксис proof assistance не выглядит такой уж сложной задачей, плюс, по дороге вы проверите, какие инструменты доказательства вы использовали.

Я не утверждал, что мы не можем перевести доказательства в формальные системы. Я говорил о том, что перевод в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована.
Боюсь, без формализации современная математика превратится в астрологию, где ваши представления будут основываться на субъективной вере/доверии к авторитету источника утверждения.

Она в каком-то смысле уже — это кризис проверяемости, о котором я писал выше. В ближайшем будущем, когда узкую специализированную область будут понимать не 10 человек в мире (как сейчас в алгебраической геометрии), а 1, придется разрабатывать новые подходы, поскольку верификация сообществом станет принципиально невозможна.
Потому полагаться в этом вопросе на более надежные вычислители – хорошая идея.

Я полностью согласен с тем, что мы хотим всё формализовать и проверять вычислителями, но этого не происходит — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно. Нам безусловно придется рано или поздно этим заниматься, когда кризис станет более очевиден, однако для этого нужны будут более эффективные инструменты.

Вроде есть проект в рамках которого "кодируют" "всю математику".

Так что есть свет в конце тоннеля.

И это странно, потому что язык математики изначально формален.
Проблема видится исключительно в инструментах, надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.
Он «формален» только формально (no pun intended) — мат. понятия вводятся формально для человека, но это даже не близко тот уровень формальности, который требуется для кодирования.

Перевод математики в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно.
надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.

Сначала нужно разработать более эффективные подходы, иначе кодирование текущей математики займет несколько веков.
Сначала нужно разработать более эффективные подходы
То есть, нужен другой язык. То, что сейчас есть — исчисление предикатов — это как ассемблер: близко к машине, но очень многословно.

Рано останавливаться.


Во-первых, разные пруфассистанты реализуют немного разные логики. Например, есть такая штука, как аксиома K, с которой доказательства некоторых вещей становятся сильно проще, но, с другой стороны, она несовместима с некоторыми видами оснований математики.
Во-вторых, мы ещё не очень хорошо понимаем метатеорию. Например, работа с коданными — это боль, и доказать, что 1 : 1 : 1 : ... пропозиционально равно map suc (0 : 0 : 0 : ...), довольно тяжко в коке и практически невозможно в идрисе (по крайней мере, у меня в нём не получилось).

А что об агде?

А там есть разные настройки. Конкретно про К — по крайней мере, в стандартной библиотеке стараются доказывать вещи без неё, чтобы можно было быть совместимым с HoTT.

41 положительнач оценка статьи не может ошибаться.

Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.