Он «формален» только формально (no pun intended) — мат. понятия вводятся формально для человека, но это даже не близко тот уровень формальности, который требуется для кодирования.
Перевод математики в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно.
надо остановиться на одном proof assistant и наработать библиотеку понятий, аксиом и доказанных теорем.
Сначала нужно разработать более эффективные подходы, иначе кодирование текущей математики займет несколько веков.
Относительно небезопасно, лучше - отдельным приложением. С точки зрения векторов атаки, рассматриваемых в статье, не важно оффлайн или онлайн, важно, что расширение фундаментально более уязвимо.
Записать её в терминах логики, реализуемой чекером.
Это не означает автоматически, что мы корректно закодировали новые понятия и объекты, нам так или иначе нужна внешняя проверка.
Учитывая, что в человекочитаемом виде в статье это всё занимает страницы три-четыре, в итоге получается плюс-минус то же. Да и по внешнему виду тоже: сравните, например, определение системы типов в машинопонятном виде выше с её определением в статье для людей:
Здорово, что такой подход работает в вашей области. Но это не означает, что мы получим аналогичный коэффициент «выгоды» для других областей — в эту пользу говорит не закодированность большей части математики.
А ничего лучше нет. Можно, конечно, ручкой и бумажкой, но надёжность и доверие таким доказательствам падают даже для очень маленьких групп теорем. В чужих статьях, отрецензированных, опубликованных, доложенных на конференциях, и так далее, я ошибки находил.
Поэтому я утверждаю, что нам нужны будут новые инструменты. В данный момент, используя кодирование, мы делаем двойную работу — нужно, условно, Х времени, чтобы понять объект, который мы кодируем, и Х10, чтобы его закодировать.
Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.
Может быть, но таково состояние вещей в данный момент.
В моем понимании, если вы не способны выразить ваше доказательство в какой-либо формальной системе, то лучше считать что у вас нет полного доказательства, а только его набросок. Дальше уже перевести из одной формальной системы в синтаксис proof assistance не выглядит такой уж сложной задачей, плюс, по дороге вы проверите, какие инструменты доказательства вы использовали.
Я не утверждал, что мы не можем перевести доказательства в формальные системы. Я говорил о том, что перевод в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована.
Боюсь, без формализации современная математика превратится в астрологию, где ваши представления будут основываться на субъективной вере/доверии к авторитету источника утверждения.
Она в каком-то смысле уже — это кризис проверяемости, о котором я писал выше. В ближайшем будущем, когда узкую специализированную область будут понимать не 10 человек в мире (как сейчас в алгебраической геометрии), а 1, придется разрабатывать новые подходы, поскольку верификация сообществом станет принципиально невозможна.
Потому полагаться в этом вопросе на более надежные вычислители – хорошая идея.
Я полностью согласен с тем, что мы хотим всё формализовать и проверять вычислителями, но этого не происходит — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно. Нам безусловно придется рано или поздно этим заниматься, когда кризис станет более очевиден, однако для этого нужны будут более эффективные инструменты.
Я не совсем корректно выразился: как показывает статья выше, кодирование многократно более времязатратно (предполагая, что вобще осуществимо), чем классическое доказательство, однако, действительно не будет требовать дополнительной "внешней" проверки сообществом.
Тот факт, что на классическую проверку уходят годы, означает, в текущих реалиях, что на кодирование могут уйти десятилетия (предполагая, что сложность проверки, или сложность самой теоремы, скоррелирована со сложностью кодирования), откуда можно сделать вывод о необходимости принципиально новых способов кодирования. В пользу этого предположения дополнительно говорит факт практически полного отсутствия возможности алгоритмической проверки подавляющего большинства мат. отраслей: кодировать выходит слишком долго.
Де-факто проверка сообществом, в данный момент, это единственный способ верификации.
В случае чекера мне тоже не все очевидно: что делать, например, когда создается новая область? Как проверить, что новые понятия и объекты корректно закодированы? Для меня это выглядит так, что все равно потребуется внешняя проверка, но тогда мы возвращаемся к изначальной теме - будет ли в таком случае профит, кроме самого факта кодирования.
Пусть мы закодировали и верифицировали, это позволяет нам доказать Х теорем внутри данной области. Но, во-первых, каждая новая отрасль будет требовать нового кодирования и верификации, во-вторых, мы тратим на это время, причем значительное. Мне не очевидно, что это жизнеспособный способ доказательства.
Естественным образом мы приходим к кризису проверяемости в науке.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?
Более того, даже вне контекста формализованных проверок, в случае математики, мы начинаем наблюдать разделение на школы — японская школа, считающая abc conjecture доказанной, и европейская школа (включая, что иронично, собственно Шольце), отрицающая доказательство Мотидзуки. Иными словами, мы вплотную подошли к моменту, когда доказательство приходится принимать «на веру». Судя по всему, это первые звоночки надвигающегося кризиса.
Резюмируя: мы уже не справляемся с классической проверкой отдельных теорем, а формальное кодирование требует кратно больших усилий. Соответственно, нужно изобретать совершенно новую парадигму для кодирования, поскольку в текущем виде это тупиковый подход.
В каком-то смысле данная статья демонстрирует степень неэффективности формального кодирования теорем:
По словам одного из помощников Йохана Коммелина, Lean-версия доказательства Шольце включат десятки тысяч строк кода — она примерно в 100 раз больше, чем оригинальная версия
У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.
Firefox не секьюрен.
В отличие от Chromium-based браузеров, у Firefox на андроиде полностью отсутствует sandboxing как таковой, и помимо этого он не имеет ряда механизмов защиты от эксплоитов (цитата):
Avoid Gecko-based browsers like Firefox as they're currently much more vulnerable to exploitation and inherently add a huge amount of attack surface. Gecko doesn't have a WebView implementation (GeckoView is not a WebView implementation), so it has to be used alongside the Chromium-based WebView rather than instead of Chromium, which means having the remote attack surface of two separate browser engines instead of only one. Firefox / Gecko also bypass or cripple a fair bit of the upstream and GrapheneOS hardening work for apps. Worst of all, Firefox runs as a single process on mobile and has no sandbox beyond the OS sandbox. This is despite the fact that Chromium semantic sandbox layer on Android is implemented via the OS isolatedProcess feature, which is a very easy to use boolean property for app service processes to provide strong isolation with only the ability to communicate with the app running them via the standard service API. Even in the desktop version, Firefox's sandbox is still substantially weaker (especially on Linux, where it can hardly be considered a sandbox at all) and lacks support for isolating sites from each other rather than only containing content as a whole.
Рефлексируя далее, если уж автор додумался, что мы не знаем как реальный мир устроен, вместо того, чтобы банально пропагандировать свою позицию, неплохо бы предпринять какие-то шаги к тому, чтобы решить эту проблему.
Правда, пока 30 лет размышляешь о природе сознания\ разрабатываешь теорию всего\ медитируешь в пещере\ pick your option лайков и репостов не соберешь)
Ну и в качестве эксперимента пульнул переводом плюгавенькой философщины (ушло в пределах 20 минут). И пожалуйста, по количеству просмотров и одобрений он за несколько часов обошел месячную статистику самой техничной статьи цикла
Это как раз ожидаемо — у статьи высокий engagement, она должна «задевать за живое» (я тоже, как видите, не устоял), в то время как технические статьи требуют вчитывания и имеют определенный порог вхождения.
И потом комментаторы удивляются, дескать пикабу притащили.
Естественный отбор, ничего не поделаешь, в топе всегда будут «спорные» (а ещё лучше — hate speech) материалы (на этом целые платформы строятся, например, твиттер). Остается только задать себе вопрос, чего вы хотите, как автор — просмотров, лайков и репостов, или донести что-то до читателя.
Я полагаю, что я защищаю простое признание того, что никакая теория или теология не могут воздать должное тайне нашего существования. Этот скромный агностицизм, как мне кажется, и выбрал бы Homo sapiens.
Этот абзац в совокупности с описанием автора
John Horgan directs the Center for Science Writings at the Stevens Institute of Technology. His books include The End of Science, The End of War and Mind-Body Problems, available for free at mindbodyproblems.com.
обнажает суть данной пропаганды — Джон выбрал себе комфортную идею и без каких-то конкретных аргументов обличает «нео-геоцентристов», браво!
Не очень понятно, зачем писать огромную статью, которая тезисно сводится к «никакая теория или теология не могут воздать должное тайне нашего существования».
«Спорный термин, который в общем описывает проявление эмерджентных процессов в физической системе» — чем такой (очередной максимально отстраненный) вариант не устраивает?
Такое определение имеет смысл только в редуктивном физикализме. Нередуктивный физикализм, дуализм, солипсизм (любая из гипотез, в которых сознание имеет собственный онтологический статус либо не сводится к физическим системам) будут требовать, как минимум, включения субъективных переживаний.
Навряд ли будет конкретный ответ, типа сознание образуется из темной материи/флуктуаций вакуума/суперпозиции ионов в цитоскелете — хотя многие видно именно этого и ждут.
В сущности, вы сформулировали трудную проблему, эмерджентным образом. Описание сознания, судя по всему, будет требовать новых отраслей науки, у которых будет инструментарий для описания субъективных переживаний.
Это в том случае, если и отправитель и получатель пользуется ProtonMail.
Не, это во всех случаях.
Логику включайте.
И вам того же.
Сообщения на не протоновские аккаунты отправляются без шифрования, но это не значит, что отправленное сообщение при этом сохраняется в незашифрованном виде на сервере. Открытая архитектура позволяет убедиться, в каком виде данные куда отправляются.
ProtonMail's zero access architecture means that your data is encrypted in a way that makes it inaccessible to us. Data is encrypted on the client side using an encryption key that we do not have access to. This means we don't have the technical ability to decrypt your messages, and as a result, we are unable to hand your data over to third parties. With ProtonMail, privacy isn't just a promise, it is mathematically ensured. For this reason, we are also unable to do data recovery. If you forget your password, we cannot recover your data.
Более того, протон опенсорсный, можно пойти и проверить самому.
Это вопрос личных предпочтений, у вас специфичный юзеркейс — вам подошел бы, наверное, профессиональный граф. планшет.
S7+ (12.4 дюйма) — практически А4, и он мне оказался неудобен (слишком большой) для письма, во всех положениях, кроме лежащего на столе. Вопрос масштаба решается обычным зумом (Samsung Notes, OneNote).
Я люблю, когда у вещи есть одна и конкретная цель. Можно сказать, unix way in real life. А планшет, он, наверное, не только для письма: там тебе и youtube, и игры, и прочее.
А это уже проблема конкретного юзера, так сказать)
Я думаю, если бы у меня была необходимость не просто в письме, а еще и в презентациях, например, то в сторону планшета я бы уже посмотрел.
Планшет дает в целом очень широкие возможности для работы и рисёрча — аннотирование pdfок, гиперссылки, смешанные письменно-печатные заметки, импорт картинок\таблиц.
После осознания того, насколько неэффективно получается постоянно переключаться между печатным и электронным медиумом, если с текстом нужно производить какой-то анализ\синтез (кроме тех случаев, конечно, когда заметки пишутся, чтобы не забыть в будущем), другие формы письма сами собой отпадают.
Перевод математики в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно.
Сначала нужно разработать более эффективные подходы, иначе кодирование текущей математики займет несколько веков.
Относительно небезопасно, лучше - отдельным приложением. С точки зрения векторов атаки, рассматриваемых в статье, не важно оффлайн или онлайн, важно, что расширение фундаментально более уязвимо.
Это не означает автоматически, что мы корректно закодировали новые понятия и объекты, нам так или иначе нужна внешняя проверка.
Здорово, что такой подход работает в вашей области. Но это не означает, что мы получим аналогичный коэффициент «выгоды» для других областей — в эту пользу говорит не закодированность большей части математики.
Поэтому я утверждаю, что нам нужны будут новые инструменты. В данный момент, используя кодирование, мы делаем двойную работу — нужно, условно, Х времени, чтобы понять объект, который мы кодируем, и Х10, чтобы его закодировать.
Не похоже, что у данной проблемы будет простое решение. Наиболее вероятно, нам понадобится интерфейс вида мозг-компьютер, по типу нейралинка, чтобы мат. понятия реализовывать сразу в виде кода, минуя промежуточный этап.
Может быть, но таково состояние вещей в данный момент.
Я не утверждал, что мы не можем перевести доказательства в формальные системы. Я говорил о том, что перевод в формальную систему занимает кратно большие усилия, а потому нереалистичен с текущими инструментами. Подавляющая часть математики не закодирована.
Она в каком-то смысле уже — это кризис проверяемости, о котором я писал выше. В ближайшем будущем, когда узкую специализированную область будут понимать не 10 человек в мире (как сейчас в алгебраической геометрии), а 1, придется разрабатывать новые подходы, поскольку верификация сообществом станет принципиально невозможна.
Я полностью согласен с тем, что мы хотим всё формализовать и проверять вычислителями, но этого не происходит — кодирование даже простых теорем текущими инструментами слишком сложно и времязатратно. Нам безусловно придется рано или поздно этим заниматься, когда кризис станет более очевиден, однако для этого нужны будут более эффективные инструменты.
Я не совсем корректно выразился: как показывает статья выше, кодирование многократно более времязатратно (предполагая, что вобще осуществимо), чем классическое доказательство, однако, действительно не будет требовать дополнительной "внешней" проверки сообществом.
Тот факт, что на классическую проверку уходят годы, означает, в текущих реалиях, что на кодирование могут уйти десятилетия (предполагая, что сложность проверки, или сложность самой теоремы, скоррелирована со сложностью кодирования), откуда можно сделать вывод о необходимости принципиально новых способов кодирования. В пользу этого предположения дополнительно говорит факт практически полного отсутствия возможности алгоритмической проверки подавляющего большинства мат. отраслей: кодировать выходит слишком долго.
Де-факто проверка сообществом, в данный момент, это единственный способ верификации.
В случае чекера мне тоже не все очевидно: что делать, например, когда создается новая область? Как проверить, что новые понятия и объекты корректно закодированы? Для меня это выглядит так, что все равно потребуется внешняя проверка, но тогда мы возвращаемся к изначальной теме - будет ли в таком случае профит, кроме самого факта кодирования.
Пусть мы закодировали и верифицировали, это позволяет нам доказать Х теорем внутри данной области. Но, во-первых, каждая новая отрасль будет требовать нового кодирования и верификации, во-вторых, мы тратим на это время, причем значительное. Мне не очевидно, что это жизнеспособный способ доказательства.
В данный момент, когда классическая проверка доказательства может занимать, буквально, годы (как в случае, например, с abc conjecture), сколько займет кодирование? Десятилетия?
Более того, даже вне контекста формализованных проверок, в случае математики, мы начинаем наблюдать разделение на школы — японская школа, считающая abc conjecture доказанной, и европейская школа (включая, что иронично, собственно Шольце), отрицающая доказательство Мотидзуки. Иными словами, мы вплотную подошли к моменту, когда доказательство приходится принимать «на веру». Судя по всему, это первые звоночки надвигающегося кризиса.
Резюмируя: мы уже не справляемся с классической проверкой отдельных теорем, а формальное кодирование требует кратно больших усилий. Соответственно, нужно изобретать совершенно новую парадигму для кодирования, поскольку в текущем виде это тупиковый подход.
У группы математиков ушло пол года на кодирование одной теоремы. Напрашивается вопрос, сколько «обычных» теорем можно бы было доказать за это время.
В отличие от Chromium-based браузеров, у Firefox на андроиде полностью отсутствует sandboxing как таковой, и помимо этого он не имеет ряда механизмов защиты от эксплоитов (цитата):
Как и в аналогичных случаях. Например, при инверсии электронных населённостей система будет иметь отрицательную температуру.
Правда, пока 30 лет размышляешь о природе сознания\ разрабатываешь теорию всего\ медитируешь в пещере\ pick your option лайков и репостов не соберешь)
Это как раз ожидаемо — у статьи высокий engagement, она должна «задевать за живое» (я тоже, как видите, не устоял), в то время как технические статьи требуют вчитывания и имеют определенный порог вхождения.
Естественный отбор, ничего не поделаешь, в топе всегда будут «спорные» (а ещё лучше — hate speech) материалы (на этом целые платформы строятся, например, твиттер). Остается только задать себе вопрос, чего вы хотите, как автор — просмотров, лайков и репостов, или донести что-то до читателя.
Этот абзац в совокупности с описанием автора
обнажает суть данной пропаганды — Джон выбрал себе комфортную идею и без каких-то конкретных аргументов обличает «нео-геоцентристов», браво!
Не очень понятно, зачем писать огромную статью, которая тезисно сводится к «никакая теория или теология не могут воздать должное тайне нашего существования».
Такое определение имеет смысл только в редуктивном физикализме. Нередуктивный физикализм, дуализм, солипсизм (любая из гипотез, в которых сознание имеет собственный онтологический статус либо не сводится к физическим системам) будут требовать, как минимум, включения субъективных переживаний.
В сущности, вы сформулировали трудную проблему, эмерджентным образом. Описание сознания, судя по всему, будет требовать новых отраслей науки, у которых будет инструментарий для описания субъективных переживаний.
Не, это во всех случаях.
И вам того же.
Сообщения на не протоновские аккаунты отправляются без шифрования, но это не значит, что отправленное сообщение при этом сохраняется в незашифрованном виде на сервере. Открытая архитектура позволяет убедиться, в каком виде данные куда отправляются.
А по делу — открытая архитектура позволяет убедиться, в каком виде данные куда отправляются.
Более того, протон опенсорсный, можно пойти и проверить самому.
S7+ (12.4 дюйма) — практически А4, и он мне оказался неудобен (слишком большой) для письма, во всех положениях, кроме лежащего на столе. Вопрос масштаба решается обычным зумом (Samsung Notes, OneNote).
А это уже проблема конкретного юзера, так сказать)
Планшет дает в целом очень широкие возможности для работы и рисёрча — аннотирование pdfок, гиперссылки, смешанные письменно-печатные заметки, импорт картинок\таблиц.
После осознания того, насколько неэффективно получается постоянно переключаться между печатным и электронным медиумом, если с текстом нужно производить какой-то анализ\синтез (кроме тех случаев, конечно, когда заметки пишутся, чтобы не забыть в будущем), другие формы письма сами собой отпадают.