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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Metamath Proof Explorer -- Theorem eulerid

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

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

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

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

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

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

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

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

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

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