Комментарии 26
Очень теорему, значит. Ну ладно
Это же явно перевод — почему нет ссылки на оригинал статьи?
Корпоративные блоги видимо не ездят по общим рельсам. На самом деле ссылка в статье на исходник есть, но она не в заголовке.
пишет Nature.
Ну и в какой момент мы скатились до того, что код в статье на хабре является просто абстрактной картинкой-иллюстрацией для привлечения внимания? Ну спасибо хоть не HTML вставили.
Что пытается донести эта статья? Что есть такой раздел математики как топология? Так мы в курсе. Что есть proof assistance? Так мы в курсе. Что кто-то назвал что-то другое революционным? Так нам плевать.
В статье ровно ноль интересной информации.
Что пытается донести эта статья? Что есть такой раздел математики как топология? Так мы в курсе. Что есть proof assistance? Так мы в курсе. Что кто-то назвал что-то другое революционным? Так нам плевать.
В статье ровно ноль интересной информации.
хабр-бизнес, ничего личного…
В каком-то смысле данная статья демонстрирует степень неэффективности формального кодирования теорем:
У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.
По словам одного из помощников Йохана Коммелина, Lean-версия доказательства Шольце включат десятки тысяч строк кода — она примерно в 100 раз больше, чем оригинальная версия
У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.
НЛО прилетело и опубликовало эту надпись здесь
Естественным образом мы приходим к кризису проверяемости в науке.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?
Более того, даже вне контекста формализованных проверок, в случае математики, мы начинаем наблюдать разделение на школы — японская школа, считающая abc conjecture доказанной, и европейская школа (включая, что иронично, собственно Шольце), отрицающая доказательство Мотидзуки. Иными словами, мы вплотную подошли к моменту, когда доказательство приходится принимать «на веру». Судя по всему, это первые звоночки надвигающегося кризиса.
Резюмируя: мы уже не справляемся с классической проверкой отдельных теорем, а формальное кодирование требует кратно больших усилий. Соответственно, нужно изобретать совершенно новую парадигму для кодирования, поскольку в текущем виде это тупиковый подход.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?
Более того, даже вне контекста формализованных проверок, в случае математики, мы начинаем наблюдать разделение на школы — японская школа, считающая abc conjecture доказанной, и европейская школа (включая, что иронично, собственно Шольце), отрицающая доказательство Мотидзуки. Иными словами, мы вплотную подошли к моменту, когда доказательство приходится принимать «на веру». Судя по всему, это первые звоночки надвигающегося кризиса.
Резюмируя: мы уже не справляемся с классической проверкой отдельных теорем, а формальное кодирование требует кратно больших усилий. Соответственно, нужно изобретать совершенно новую парадигму для кодирования, поскольку в текущем виде это тупиковый подход.
Вот пруфчекер Globular, где доказательства строятся в виде картинок по принципу «раскрась сам».
golem.ph.utexas.edu/category/2015/12/globular.html
Он для специальной области, не для всего. Придумали, что характерно, посторонние люди (квантовые физики), у которых взгляд не замылен.
golem.ph.utexas.edu/category/2015/12/globular.html
Он для специальной области, не для всего. Придумали, что характерно, посторонние люди (квантовые физики), у которых взгляд не замылен.
НЛО прилетело и опубликовало эту надпись здесь
Я не совсем корректно выразился: как показывает статья выше, кодирование многократно более времязатратно (предполагая, что вобще осуществимо), чем классическое доказательство, однако, действительно не будет требовать дополнительной "внешней" проверки сообществом.
Тот факт, что на классическую проверку уходят годы, означает, в текущих реалиях, что на кодирование могут уйти десятилетия (предполагая, что сложность проверки, или сложность самой теоремы, скоррелирована со сложностью кодирования), откуда можно сделать вывод о необходимости принципиально новых способов кодирования. В пользу этого предположения дополнительно говорит факт практически полного отсутствия возможности алгоритмической проверки подавляющего большинства мат. отраслей: кодировать выходит слишком долго.
Де-факто проверка сообществом, в данный момент, это единственный способ верификации.
В случае чекера мне тоже не все очевидно: что делать, например, когда создается новая область? Как проверить, что новые понятия и объекты корректно закодированы? Для меня это выглядит так, что все равно потребуется внешняя проверка, но тогда мы возвращаемся к изначальной теме - будет ли в таком случае профит, кроме самого факта кодирования.
Пусть мы закодировали и верифицировали, это позволяет нам доказать Х теорем внутри данной области. Но, во-первых, каждая новая отрасль будет требовать нового кодирования и верификации, во-вторых, мы тратим на это время, причем значительное. Мне не очевидно, что это жизнеспособный способ доказательства.
НЛО прилетело и опубликовало эту надпись здесь
Записать её в терминах логики, реализуемой чекером.
Это не означает автоматически, что мы корректно закодировали новые понятия и объекты, нам так или иначе нужна внешняя проверка.
Учитывая, что в человекочитаемом виде в статье это всё занимает страницы три-четыре, в итоге получается плюс-минус то же. Да и по внешнему виду тоже: сравните, например, определение системы типов в машинопонятном виде выше с её определением в статье для людей:
Здорово, что такой подход работает в вашей области. Но это не означает, что мы получим аналогичный коэффициент «выгоды» для других областей — в эту пользу говорит не закодированность большей части математики.
А ничего лучше нет. Можно, конечно, ручкой и бумажкой, но надёжность и доверие таким доказательствам падают даже для очень маленьких групп теорем. В чужих статьях, отрецензированных, опубликованных, доложенных на конференциях, и так далее, я ошибки находил.
Поэтому я утверждаю, что нам нужны будут новые инструменты. В данный момент, используя кодирование, мы делаем двойную работу — нужно, условно, Х времени, чтобы понять объект, который мы кодируем, и Х10, чтобы его закодировать.
Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.
НЛО прилетело и опубликовало эту надпись здесь
Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.Почему нейроинтерфейс нужен? Они нужны, чтобы продвинуть физику. Вот здесь довольно подробно написал на эту тему. Чтобы продвинуть математические методы, кот. в первую очередь опять же нужны для построения новых физических теорий, нужен продвинутый интеллект, а это только ИИ, возможно в интерфейсе с человеком (симбиотический ИИ), см. комент в той же статье. Вообще коменты в той статье по поводу той же импликации напомнили мне средневековые схоластические споры) вроде приводят логические выводы, но результаты получаются разные.
Де-факто проверка сообществом, в данный момент, это единственный способ верификации.Как-то сомнительно для меня все это звучит.
В моем понимании, если вы не способны выразить ваше доказательство в какой-либо формальной системе, то лучше считать что у вас нет полного доказательства, а только его набросок. Дальше уже перевести из одной формальной системы в синтаксис proof assistance не выглядит такой уж сложной задачей, плюс, по дороге вы проверите, какие инструменты доказательства вы использовали.
Я охотно допускаю, что даже сотни пар просветленных глаз способны одинаково ошибаться, если у них одна и та же база знаний. Так что все вариации на тему «очевидно что A => B» приниматься на веру не должны, особенно если A и B не вполне определены формально.
Здесь я вижу полную аналогию с компиляторами высокоуровневых языков: реализовать корректный компилятор языка – сложная задача, но сделав это, вы получаете гарантии корректности конечного кода при условии выполнения вполне осознаваемых и легко проверяемых требований к высокоуровневому коду.
Так и в математике: если мы доверяем корректной реализации proof assistance, то теорему следует считать доказанной как только мы соглашаемся с аксиоматической базой и допустимыми методами выведения термов.
Боюсь, без формализации современная математика превратится в астрологию, где ваши представления будут основываться на субъективной вере/доверии к авторитету источника утверждения.
Ну и последнее, математическое утверждение корректно или не корректно независимо от того, способны ли вы осмыслить доказательство в силу своих природных ограничений. Потому полагаться в этом вопросе на более надежные вычислители – хорошая идея.
Как-то сомнительно для меня все это звучит.
Может быть, но таково состояние вещей в данный момент.
В моем понимании, если вы не способны выразить ваше доказательство в какой-либо формальной системе, то лучше считать что у вас нет полного доказательства, а только его набросок. Дальше уже перевести из одной формальной системы в синтаксис proof assistance не выглядит такой уж сложной задачей, плюс, по дороге вы проверите, какие инструменты доказательства вы использовали.
Я не утверждал, что мы не можем перевести доказательства в формальные системы. Я говорил о том, что перевод в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована.
Боюсь, без формализации современная математика превратится в астрологию, где ваши представления будут основываться на субъективной вере/доверии к авторитету источника утверждения.
Она в каком-то смысле уже — это кризис проверяемости, о котором я писал выше. В ближайшем будущем, когда узкую специализированную область будут понимать не 10 человек в мире (как сейчас в алгебраической геометрии), а 1, придется разрабатывать новые подходы, поскольку верификация сообществом станет принципиально невозможна.
Потому полагаться в этом вопросе на более надежные вычислители – хорошая идея.
Я полностью согласен с тем, что мы хотим всё формализовать и проверять вычислителями, но этого не происходит — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно. Нам безусловно придется рано или поздно этим заниматься, когда кризис станет более очевиден, однако для этого нужны будут более эффективные инструменты.
И это странно, потому что язык математики изначально формален.
Проблема видится исключительно в инструментах, надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.
Проблема видится исключительно в инструментах, надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.
Он «формален» только формально (no pun intended) — мат. понятия вводятся формально для человека, но это даже не близко тот уровень формальности, который требуется для кодирования.
Перевод математики в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно.
Сначала нужно разработать более эффективные подходы, иначе кодирование текущей математики займет несколько веков.
Перевод математики в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно.
надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.
Сначала нужно разработать более эффективные подходы, иначе кодирование текущей математики займет несколько веков.
НЛО прилетело и опубликовало эту надпись здесь
А что об агде?
Вообще, "концентрировать усилия" и "останавливаться на одном" обычно предлагают люди, которые вообще не понимают, как работает open source (и социум в целом), какая у людей бывает мотивация и пр. Довольно глупо думать, что если есть две чем-то похожих разработки и одну из них как-то насильственно свернуть, то все её разработчики тут же бросятся работать над второй. А подобные ребята обычно предполагают что-то такое у себя в голове.
41 положительнач оценка статьи не может ошибаться.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Компьютерное доказательство теории конденсированной математики — первый шаг к «великому объединению»