Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

Здравствуйте, Shmj, Вы писали:

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.
S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

Если я все правильно путаю, то в Коке и аналогах математика конструктивная, логика интуиционистская, не булева. Т.е. не работают доказательства от противного, и нужно уметь из одних утверждений производить другие гарантированно завершающимся алгоритмом (нет Тьюринг-полноты, и это важно, т.к. Тьюринг-полная программа может всегда зависнуть и тем самым служить недовычисленным доказательством любого утверждения). А посему вещественные числа и обычный матан уже довольно сложно описать (если вообще можно). Привычные определения и теоремы из матана часто подразумевают "бесконечные циклы" — пределы бесконечных последовательностей и операции с ними. Хорошо идет всякая дискретка, а с континуальными вещами уже сложно.
Ну и чисто организационно: заставить всех математиков освоить такой язык и переучиться на его использование малореально. Очень по-другому там строятся и выглядят доказательства, сам ход мысли часто очень отличается.

Здравствуйте, koenig, Вы писали:

K> ты к чему-нибудь практическому пруверы или какие-нибудь там модел-чекеры смог пристягнуть?

Если не играться, а так чтобы практика-практика, у меня был проектик на Идрисе, который генерировал код на C#, который потом использовался в одном из продуктов (GraphEditPlus). Но там примерно с тем же успехом мог бы использоваться и хаскель, и другие подобные. Особого пруверства не было, а зависимые типы использовались по мелочам, вроде сделать число аргументов у ф-ии различным в зависимости от содержания строки в первом (а-ля printf).

Здравствуйте, koenig, Вы писали:


K>я вот думаю маленькую распределенную системку на дотнете накалякать и ищу чем формальные методы могут мне помочь
K>и получается, что ничем

Tla+ Лэмплрта чем не то? Можно найти введение в это дело+видео лекции Лэмпорта. Использовались в амазон для валидации DynamoDb. Да много где использовалась, в том числе и им.

Здравствуйте, D. Mon, Вы писали:


DM>Если я все правильно путаю, то в Коке и аналогах математика конструктивная, логика интуиционистская, не булева. Т.е. не работают доказательства от противного, и нужно уметь из одних утверждений производить другие гарантированно завершающимся алгоритмом (нет Тьюринг-полноты, и это важно, т.к. Тьюринг-полная программа может всегда зависнуть и тем самым служить недовычисленным доказательством любого утверждения). А посему вещественные числа и обычный матан уже довольно сложно описать (если вообще можно). Привычные определения и теоремы из матана часто подразумевают "бесконечные циклы" — пределы бесконечных последовательностей и операции с ними. Хорошо идет всякая дискретка, а с континуальными вещами уже сложно.

Классическую логику тоже можно

example (h : ¬¬p) : p :=
by_contradiction
  (assume h1 : ¬p,
    show false, from h h1)

см. 3.5. Classical Logic здесь

DM>Ну и чисто организационно: заставить всех математиков освоить такой язык и переучиться на его использование малореально. Очень по-другому там строятся и выглядят доказательства, сам ход мысли часто очень отличается.
Всех математиков и не надо наверно, но если не проверять доказательства программно, нельзя поручиться, что в них не закралась ошибка. Не зря Воеводский занялся этой областью, его очень беспокоил этот вопрос.

Здравствуйте, pagid, Вы писали:

vsb>>Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает.
P>А не пришлось бы для действительно новых теорем каждый раз прикручивать новые расширения к языку? Отлаживать и тестировать машину вывода, видимо на примере этой самой новой теоремы

Скорее всего нет — он же Тьюринг-полный. Хотя...

Здравствуйте, kov_serg, Вы писали:

_>Некоторые утверждения не имеют доказательств и являются гипотезами которые никто не доказал и не опроверг. Что сними делать будете?

Так речь же о доказательствах...

S>>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики?
_>Для кого всё это для машин или для людей? Что от того что 44?

А что, Нельзя сдлеать язык, который был бы и для людей и для машин удобен?

Ведь для многих из нас на программном коде — понятнее чем словами.

S>>Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?
_>А нахрена? И за чей счет будет этот банкет?

Может там ошибка? Перевести и иметь формальное доказательство верности доказательства.

Здравствуйте, kov_serg, Вы писали:

_>Если эта область знаний имеет практическое приложения ошибки быстро всплывут, а если нет то и х.. с ним.

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

Здравствуйте, alzt, Вы писали:

N>>Некоторые ошибки могут "быстро всплыть" на космических аппаратах где-нибудь далеко от земли, внутри ускорителей частиц и других крайних состояниях. Как-то дорого получится, не считаешь?
A>Либо они используют только доказанные утверждения, либо надеются на авось.

Ну, не всё так просто. Не будешь ставить на гипотезы, не попьёшь шампанское на вручении Нобелевки.

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

о, "интегрировай"

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

иди сюда и далее по ссылкам
внеси свой вклад

Здравствуйте, Shmj, Вы писали:

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

Видимо потому, что разработка такого языка еще не закончена.
Сейчас идут работы в области Cubical Type Theory. Там аксиому унивалентности Воеводского сделали теоремой. Написана парочка theorem prover-ов. Только не понятно, насколько надо знать алгебраическую топологию и n-категории, чтобы въехать в это.

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

Самое удобное из того, что я видел — это Lean Theorem Prover. Но авторы не занимаются популяризацией и туториалы для дебилов пишут крайне медленно. Не знаю на счет математики, но доказывать корректность сложных мест в коде программ было бы здорово, но пока это только мечта.

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

Здравствуйте, vsb, Вы писали:

vsb>Кстати интересно. А вообще реально хотя бы то, что студентам преподают, засунуть в формализацию? Вроде как все доказательства довольно формальны и дело только за тем, чтобы написать формальный язык описания доказательства и сделать, так сказать, базу этих самых теорем и доказательств. По ней можно и учебники генерировать автоматически.

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

Здравствуйте, lpd, Вы писали:

vsb>>Кстати интересно. А вообще реально хотя бы то, что студентам преподают, засунуть в формализацию? Вроде как все доказательства довольно формальны и дело только за тем, чтобы написать формальный язык описания доказательства и сделать, так сказать, базу этих самых теорем и доказательств. По ней можно и учебники генерировать автоматически.

lpd>Есть труды Бурбаки. Только я не вижу в этом смысла, т.к. за излишняя формализация отдаляет от читателя смысл математики. Доказательство теоремы — это прежде всего выявление высокоуровневых взаимосвязей между абстрактными понятиями, а не посторение строгой логической цепочки.

Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает. Заодно всех ферма-фриков можно отсечь, например (а может быть и найти жемчужину, мало ли).

Здравствуйте, vsb, Вы писали:

vsb>Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает.
А не пришлось бы для действительно новых теорем каждый раз прикручивать новые расширения к языку? Отлаживать и тестировать машину вывода, видимо на примере этой самой новой теоремы

Здравствуйте, Shmj, Вы писали:

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.
Некоторые утверждения не имеют доказательств и являются гипотезами которые никто не доказал и не опроверг. Что сними делать будете?

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики?
Для кого всё это для машин или для людей? Что от того что 44?
S>Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?
А нахрена? И за чей счет будет этот банкет?

Здравствуйте, Shmj, Вы писали:

_>>Некоторые утверждения не имеют доказательств и являются гипотезами которые никто не доказал и не опроверг. Что сними делать будете?
S>Так речь же о доказательствах...
Некоторые доказательства стороятся на гипотезах. И не смотря на свою не доказанность успешно применяются. Например abc-гипотеза.

S>>>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики?
_>>Для кого всё это для машин или для людей? Что от того что 44?
S>А что, Нельзя сдлеать язык, который был бы и для людей и для машин удобен?
можно найти человека которуму любой наперёд заданный язык не удобен.
удобство для машин сводится к удобству для программистов, а программисты тоже люди.

S>Ведь для многих из нас на программном коде — понятнее чем словами.
это иллюзия. не всё выражается кодом и не всякий код понятен. Почитате код на J — там всё "понятнее чем словами".

S>>>Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?
_>>А нахрена? И за чей счет будет этот банкет?
S>Может там ошибка? Перевести и иметь формальное доказательство верности доказательства.
Если эта область знаний имеет практическое приложения ошибки быстро всплывут, а если нет то и х.. с ним.

Здравствуйте, Nuzhny, Вы писали:

_>>Если эта область знаний имеет практическое приложения ошибки быстро всплывут, а если нет то и х.. с ним.

N>Некоторые ошибки могут "быстро всплыть" на космических аппаратах где-нибудь далеко от земли, внутри ускорителей частиц и других крайних состояниях. Как-то дорого получится, не считаешь?

Либо они используют только доказанные утверждения, либо надеются на авось.

Здравствуйте, kov_serg, Вы писали:

_>>>Некоторые утверждения не имеют доказательств и являются гипотезами которые никто не доказал и не опроверг. Что сними делать будете?
S>>Так речь же о доказательствах...
_>Некоторые доказательства стороятся на гипотезах. И не смотря на свою не доказанность успешно применяются. Например abc-гипотеза.

Ну так просто введете эту гипотезу как аксиому

Здравствуйте, Shmj, Вы писали:

S>Ну так просто введете эту гипотезу как аксиому
Торема о не полноте как бы намекает что будет таких аксиом будет не ограничено много.

Здравствуйте, kov_serg, Вы писали:

S>>Ну так просто введете эту гипотезу как аксиому
_>Торема о не полноте как бы намекает что будет таких аксиом будет не ограничено много.

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

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

Здравствуйте, Shmj.

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде...

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно...

Metamath Proof Explorer -- Theorem eulerid

DM>Если я все правильно путаю, то в Коке и аналогах математика конструктивная, логика интуиционистская, не булева.

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

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

если смотреть на ironfleet(который типа на dafny написан и похож на то что мне нужно) — у меня такое ощущение, что если выкинуть нафиг .dfy файлы, то ошибок только меньше станет, потому что там не прямо из модели генерируется код, а используются промежуточные рассуждения которые меня только запутывают

есть сияющая вершина в виде coq, в котором есть code extraction. к сожалению, он в ocaml экстрактит, и попытка написать экстрактор в f# (что меня бы устроило полностью), кажется, сдохла. ну и coq уже тяжеловат для моих слабых мозгов.

есть куча разных систем как раз для моделирования примерно того, что мне надо, но прокинуть от них мостик до кода еще более никак, что в принципе обесценивает идею
вот t2, например — дотнетовский, работает с CTL∗ — казалось бы, то что доктор прописал для распределенной системы. но построишь в ней модель, а с сорцами связи никакой — и посадишь 100500 ошибок в процессе имплементации

как-то всё депрессивно

K>>я вот думаю маленькую распределенную системку на дотнете накалякать и ищу чем формальные методы могут мне помочь
K>>и получается, что ничем

S>Tla+ Лэмплрта чем не то? Можно найти введение в это дело+видео лекции Лэмпорта. Использовались в амазон для валидации DynamoDb. Да много где использовалась, в том числе и им.

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

Здравствуйте, koenig, Вы писали:


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

Реализацию нет, а вот алгоритм, точнее модель, да.

Здравствуйте, Shmj, Вы писали:

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

В тему: вот цитата старого поста одного профессионального математика на форуме dxdy.ru:

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

По идее, математические доказательства это строгие, правильные математические дедуктивные рассуждения. В реальной, развивавшейся математике они не всегда были окончательно формализованы (например, «Начала» Евклида содержат довольно туманные определения), и Рассел даже заявил, что «Законы мысли» Буля были «первой книгой, когда-либо написанной по математике».

https://ru.wikipedia.org/wiki/Начала_(Евклид)#.D0.9F.D0.B5.D1.80.D0.B2.D0.B0.D1.8F_.D0.BA.D0.BD.D0.B8.D0.B3.D0.B0

Для своего времени и вплоть до (примерно) XIX века «Начала» считались образцом логического изложения математической теории. Структура трудов Декарта, Ньютона и даже Спинозы строилась по образцу «Начал». Однако уже в античные времена были критически отмечены некоторые недостатки евклидовского труда — например, Архимед обосновал необходимость добавить «аксиому Архимеда» (которую сформулировал ещё Евдокс, живший до Евклида). Со временем число признанных недостатков постепенно увеличивалось. Современные взгляды на обоснование, содержание и методы как геометрии, так и арифметики существенно отличаются от античных[13].

Прежде всего, следует отметить, что сейчас прямая понимается как линия бесконечной длины. Античные учёные полностью избегали понятия актуальной бесконечности, у Евклида всюду используются только конечные отрезки прямой[14]. Видимо, по этой причине постулат параллельности Евклида сформулирован довольно громоздко — зато он имеет локальный характер, то есть описывает событие на ограниченном участке плоскости, в то время как, например, аксиома Прокла («через точку вне прямой проходит только одна прямая, параллельная данной») утверждает факт параллельности, который требует рассмотрения всей бесконечной прямой[15]. Ещё одной архаичной особенностью «Начал» является ограничение только двумя видами кривых — прямыми и окружностями, которые греки считали единственно совершенными[16], а также чрезмерно узкое понятие числа, которое не включало иррациональных чисел и поэтому вынудило античных математиков без особой нужды ввести параллельное с арифметикой исчисление «геометрических величин» («геометрическая алгебра», книга II «Начал»)[17].

Многие комментаторы Евклида отмечали, что данные им определения геометрических понятий бессодержательны и создают не более чем наглядный образ — например, «линия есть длина без ширины». Фактически подобные «определения» нигде далее в тексте не используются, ни одна теорема на них не опирается[13]. Излишним оказался, как уже говорилось выше, и IV постулат Евклида о равенстве всех прямых углов, его можно доказать как теорему[18][19].

Далее, по замыслу все доказательства теорем должны вытекать из явно сформулированных аксиом. На самом деле многие факты у Евклида опираются на подразумеваемую или наглядную очевидность. Прежде всего это касается понятия движения, которое неявно используется во многих местах — например, при наложении треугольников для доказательства признаков их равенства. Уже Прокл отметил этот факт как существенный методический пробел. Аксиом движения Евклид не дал — возможно, чтобы не смешивать высокую геометрию с «низкой» механикой. Современные авторы аксиоматики предусматривают специальную группу «аксиом конгруэнтности» [20][21].

Уже в доказательстве самого первого предложения («на любом отрезке можно построить равносторонний треугольник») Евклид подразумевает, что две окружности радиуса R, чьи центры находятся на расстоянии R, пересекаются в двух точках. Ни из каких аксиом это не следует[22]; для логической полноты следовало бы добавить аксиому непрерывности. Аналогичные упущения имеют место для пересечения прямой и окружности[23], в употреблении неопределяемого понятия «находиться между» (для точек) и в ряде иных мест. Аксиоматика Евклида не позволяет, например, доказать, что не существует прямой, проходящей через все три стороны треугольника.

Многочисленные комментаторы Евклида делали неоднократные попытки исправить отмеченные недочёты — было увеличено число аксиом, уточнены формулировки и доказательства[13]. Некоторые комментаторы (например, Теон Александрийский и Христофор Клавиус) при переиздании вносили свои поправки прямо в евклидовский текст. Пересмотренная и значительно дополненная версия аксиоматики, предложенная Пьером Эригоном в 1632 году, оказалась неудачной[24]. Первым крупным достижением в этом направлении стала монография «Лекции по новой геометрии» немецкого математика Морица Паша (1882)[25]. Завершением стала современная аксиоматика Гильберта для геометрии (1899 год). Она, а также различные её вариации логически полны и нигде не опираются на интуитивную очевидность[26].

Здравствуйте, koenig, Вы писали:

K>как-то всё депрессивно
А чем не зашёл Linq to Z3?

K>>как-то всё депрессивно
S>А чем не зашёл Linq to Z3?

я его как-то пропустил
спасибо, буду изучать

Здравствуйте, koenig, Вы писали:


K>есть сияющая вершина в виде coq, в котором есть code extraction. к сожалению, он в ocaml экстрактит, и попытка написать экстрактор в f# (что меня бы устроило полностью), кажется, сдохла. ну и coq уже тяжеловат для моих слабых мозгов.

есть F*, умеет экстрактить в F#, и имеет Ocaml-овский (или F# синтаксис). я как-то игрался, довольно интересная штука, хороший и понятный туториал.

MH>есть F*, умеет экстрактить в F#, и имеет Ocaml-овский (или F# синтаксис). я как-то игрался, довольно интересная штука, хороший и понятный туториал.

спасибо, посмотрю!

K>>есть сияющая вершина в виде coq, в котором есть code extraction. к сожалению, он в ocaml экстрактит, и попытка написать экстрактор в f# (что меня бы устроило полностью), кажется, сдохла. ну и coq уже тяжеловат для моих слабых мозгов.

MH>есть F*, умеет экстрактить в F#, и имеет Ocaml-овский (или F# синтаксис). я как-то игрался, довольно интересная штука, хороший и понятный туториал.

а компилировать код экстракченый в f# получалось?

Здравствуйте, koenig, Вы писали:


K>а компилировать код экстракченый в f# получалось?
сам не пробовал, но в доке сказано что может.

Здравствуйте, Shmj, Вы писали:

S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.

S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?

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

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

это будет большой шаг для систематизации.