VK
Нотация есть и была до него. Но в других головах - уже другая. :)
Size: a a a
2019 October 07
МБ
А почему нельзя сделать логичный завершающий шаг — генерировать представление в LaTeX, в духе Fortress? Зачем вообще оставлять лазейку для неформальности? :)
Затем, что математики не работают в формальных системах. Да и не смогут работать, потому что некоторые доказательства, понятные человеку неформально, формально могут занимать гигабайты текста, не понятного никому. Пользы от таких доказательств нет.
AT
Затем, что математики не работают в формальных системах. Да и не смогут работать, потому что некоторые доказательства, понятные человеку неформально, формально могут занимать гигабайты текста, не понятного никому. Пользы от таких доказательств нет.
Если говорить про генерацию LaTeX в отрыве от потенциальных гигабайтов информации, то по крайней мере Isabelle, Coq и Agda это позволяют. По крайней мере в виде LaTeX-комментариев и указанием что из формального текста попадёт в сгенерированный LaTeX-файл, а что можно опустить.
AT
Затем, что математики не работают в формальных системах. Да и не смогут работать, потому что некоторые доказательства, понятные человеку неформально, формально могут занимать гигабайты текста, не понятного никому. Пользы от таких доказательств нет.
неформальная понятность ещё требует подтверждения на корректность...
K
неформальная понятность ещё требует подтверждения на корректность...
проверку корректности производят люди, которым приходится верить. И если люди не смогут проверить корректность формального утверждения из-за того, что оно слишком большое, то людям придётся верить программе, которая проверит это утверждение за них :) Если я не ошибаюсь, так доказывалась теорема о четырёх красках
AT
проверку корректности производят люди, которым приходится верить. И если люди не смогут проверить корректность формального утверждения из-за того, что оно слишком большое, то людям придётся верить программе, которая проверит это утверждение за них :) Если я не ошибаюсь, так доказывалась теорема о четырёх красках
Хорошо, что уже есть формально верифицированное доказательство за авторством Georges Gonthier
K
доказательство чего?
МБ
Если говорить про генерацию LaTeX в отрыве от потенциальных гигабайтов информации, то по крайней мере Isabelle, Coq и Agda это позволяют. По крайней мере в виде LaTeX-комментариев и указанием что из формального текста попадёт в сгенерированный LaTeX-файл, а что можно опустить.
Интересно. Можно где-нибудь посмотреть примеры?
K
Хорошо, что уже есть формально верифицированное доказательство за авторством Georges Gonthier
Всё, понял
AT
Интересно. Можно где-нибудь посмотреть примеры?
Про Isabelle написно в tutorial https://isabelle.in.tum.de/dist/Isabelle2019/doc/tutorial.pdf начиная со страницы 53.
МБ
неформальная понятность ещё требует подтверждения на корректность...
Проблема же в том, что самим математикам, собственно, не особо интересна формальная корректность. У них же цель строить математические конструкции и методы и решать задачки физиков, химиков и прочих деятелей. В первом случае формальные методы иногда подходят (алгебраическая топология), а иногда не подходят, потому что математики не хотят формализовывать 100500 лет предыдущей математики, чтобы написать статью в своём предмете. А писать статьи с новыми результатами надо, потому что иначе денежек не заплатят.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
МБ
Про Isabelle написно в tutorial https://isabelle.in.tum.de/dist/Isabelle2019/doc/tutorial.pdf начиная со страницы 53.
А... Ну я бы хотел посмотреть на каком-нибудь реальном примере.
А
Проблема же в том, что самим математикам, собственно, не особо интересна формальная корректность. У них же цель строить математические конструкции и методы и решать задачки физиков, химиков и прочих деятелей. В первом случае формальные методы иногда подходят (алгебраическая топология), а иногда не подходят, потому что математики не хотят формализовывать 100500 лет предыдущей математики, чтобы написать статью в своём предмете. А писать статьи с новыми результатами надо, потому что иначе денежек не заплатят.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
погодите ка
А
я всегда думал, что теорвер формализован и обоснован
А
да и диффуры в принципе тоже
А
ну по крайней мере пока к численным методам не переходить, хотя и у них вроде бы есть математический формализм с обоснованием почему эти методы собственно сходятся и при каких условиях
AT
Проблема же в том, что самим математикам, собственно, не особо интересна формальная корректность. У них же цель строить математические конструкции и методы и решать задачки физиков, химиков и прочих деятелей. В первом случае формальные методы иногда подходят (алгебраическая топология), а иногда не подходят, потому что математики не хотят формализовывать 100500 лет предыдущей математики, чтобы написать статью в своём предмете. А писать статьи с новыми результатами надо, потому что иначе денежек не заплатят.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
Во втором случае формальные методы подходят редко, потому что до сих пор нет нормальной формализации дифф. уров и теорвера. Что-то там наклёвывается, но оно очень примитивное и поверхностное до сих пор. И этот метод будет точно крайне неудобным в математических рассуждениях, потому что в конструктивных теориях постоянно вылезают оговорки о примерных равенствах (с точно до эпсилон). Любая сложная математическая задача в этом просто утонет.
На днях математики обсуждали эти вопросы: https://t.me/practical_fm/2511
МБ
я всегда думал, что теорвер формализован и обоснован
В классической математике - да. А в конструктивной 50/50. Некоторые важные теоремы не выполняются, а выполняются их аналоги, с которомы тяжело работать. Собственно, главное ожидание от HoTT, что он поможет избавиться от этих проблем. Но пока таких достижений нет.
AT
В классической математике - да. А в конструктивной 50/50. Некоторые важные теоремы не выполняются, а выполняются их аналоги, с которомы тяжело работать. Собственно, главное ожидание от HoTT, что он поможет избавиться от этих проблем. Но пока таких достижений нет.
Формализация в классической логике - тоже формализация, на конструктивной свет клином, в принципе, не сошёлся. Люди во всю пользуются HOL4, HOL Light и Isabelle/HOL, не считая мелких брызг.
AT
А... Ну я бы хотел посмотреть на каком-нибудь реальном примере.
Подозреваю, половина Archive of Formal Proofs - примеры. БОльшая, половина. 😊