М.Двач / Математика

132 Кб, 800x1122
Metamath 28 мая 2017, 16:43 19319 В конец треда | Веб

Ранее я создал Мендельсона-тред, теперь хочу обратить внимание на другую достаточно клёвую вещь: Metamath.
(Это связано с основаниями математики, но не спешите отчаиваться)

В данном треде я постараюсь ответить на все возникшие у анонов вопросы. Его вроде надо сделать модерируемым.

FAQ:
1)Что это?
Это теория типов для формального доказательств первопорядковых языков. Ну то есть язык программирования для ZFC, NBG, геометрии (Тарского) и ещё много чего первопорядкового.
Всё это доступно онлайн в удобном гипертекстовом виде.

2)Какие профиты?
а) Очень большая библиотека доказательств, легко читается. Имеет достаточно долгую историю - с девяностых.
б) Пруфассистант: два режима, как в Coq: либо конструируешь доказательство, либо интерактивный режим.
в) Непосредственно прилагается самоучитель.
г) Простой (300 строк на питоне) верификатор доказательств.
д) Имеет модель в ZFC. (самая мякотка, смотри пункт 3)
е) Живое коммьюнити.

3) Какие задачи?
Есть такая статья: http://us.metamath.org/ocat/model/model.pdf
Не знаю как анону, но мне было бы очень любопытно в ней разобраться.

4) Почему "лучше" чем HoTT, Coq, HOL и т.д.?
Да потому что ZFC и логика предикатов - это математический стандарт де-факто, поэтому знание metamath может помочь вам понимать беглую речь преподавателей в институте. (А не страдать по крайностям "это очевидно" и "ничерта не понятно".)

Смело задавайте вопросы и высказывайте мнения.

Ответы1933819355193561936634994

127 Кб, 512x382
2 28 мая 2017, 19:49 2 19338

>>19319 (OP)
> знание metamath может помочь вам понимать беглую речь преподавателей в институте

Ответы19340

3 28 мая 2017, 20:05 3 19340

>>19338
Ну а что, предикат калкулус для того и нужен, чтобы понимать логические переходы.

харе лямбда, харе барендрехт 4 29 мая 2017, 13:40 4 19355

20 Кб, 524x43726 Кб, 562x448246 Кб, 736x732

>>19319 (OP)
4ый пункт улыбнул. Я тебе даже поясню, в чем ты не прав:
1) вот смотри, 1ый вариант куба Барендрегта это типизированные лямбда-исчисления, связанные между собой отношением включения (т.е. правый верхний дальний угол - самый упакованный вариант, он соответствует CoC, calculus of construction, это исчисление является основой Кока).
2) 2ой куб - соответствующие первому логические системы, которые представимы в соответствующей лямбде из 1го куба. Первичная логика предикатов соответствует правому нижнему переднему углу куба и т.о. лямбда-Р исчислению, предложенному независимо де Брауном и Говардом, в нем выразим т.н. изоморфизм Карри-Говарда.
3) из вышесказанного очевидно, что исчисление предикатов и ZFC легко и просто выразимо в Коке, ценители могут даже исключенное третье использовать. Собственно, ZFC в Коке давно есть https://github.com/coq-contribs/zfc

Ответы34990

5 29 мая 2017, 14:18 5 19356

57 Кб, 706x565119 Кб, 809x70821 Кб, 442x270

>>19319 (OP)
Посмотрел по диагонали статью http://us.metamath.org/ocat/model/model.pdf синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна (пики 2 и 3). Для подобных языков лямбда - то что доктор прописал, что-то лучше и проще придумать нереально.

Ответы19357

72 Кб, 870x293
6 29 мая 2017, 14:26 6 19357

>>19356
>синтаксис этого прувера (пик1) напоминает AUTOMATH де Брауна
Добавлю, что с той разницей, что де Браун не ограничивал себя какой-то конкретной логической системой.

Ответы19359

7 29 мая 2017, 19:06 7 19359

>>19357
1) И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
2) Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.

Моя цель - проверка домашек на доказательство. (Без стогости формальной системы - беда, плыву). ДЗ - из всяких классических учебников типа Зорича, Шеня, Шварца и т.д.
Что лучше всего использовать, чтобы быть уверенным в истинности своих утверждений?

Множества, в том же Coq - искуственно сконструированы в Ensembles чёрт ногу сломит и нет обширной библиотеки.

HoTT - слишком инновационно и никто другой не будет понимать.

Mizar - выглядит подозрительно, не разбирался в нём.

Metamath - вроде ОК же, разве не лучший вариант?
Что взамен предлагаешь? (Буду признателен.)

Ответы19362

8 29 мая 2017, 20:45 8 19362

>>19359
>И где сейчас AUTOMATH? Почему он не используется широко?(риторический вопрос)
Да нет, не риторический. Причина в том, что там слишком много ручной работы, перевести книгу в этот формат это очень трудозатратно, на примере Grundlagen Ландау можно увидеть, что это пиздецки тяжелый труд. https://www.cs.ru.nl/~freek/aut/
>Какое средство верификации всяких домашек на доказательство теорем, по-твоему, следует использовать? А то с этим проблемы постоянно.
Кок жи. Единственный нормальный кроссплатформенный прувер с человеческим лицом, годящийся для всего от домашек до сколь угодно серьезной математики.

9 29 мая 2017, 21:03 9 19364

Я вот думаю, что вы, господа, занимаетесь формализмом, логикой, онанизмом - в общем, чем угодно, только не реальной математикой.
Метаматематика - не математика, а бесплодная мастурбация. И этим всё сказано.

Ответы19367

10 29 мая 2017, 21:24 10 19366

>>19319 (OP)
> http://us.metamath.org/index.html
> A Java applet that demonstrates simple proofs.
Эх, вернул себе свой 1996!..

Выглядит как-то заброшено. Неудивительно, что все кок вместо этого советуют. Но тебе же не статьи на нем писать, тебе надо свою вполне конкретную задачу решить, так что не вижу смысла тебе следовать этим советам. К тому же когда надо будет - перекатишься без проблем: все-таки между любыми двумя пруферами гэп намного меньше, чем между пруфером и доказательствами на бумаге.

Кстати, а что с мендельсонотредом? Забросил или не взлетел?

Ответы19581

11 29 мая 2017, 21:26 11 19367

>>19364
А математика тогда что?

Ответы19368

12 29 мая 2017, 23:26 12 19368

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

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

Во! Математика это короче духовность, а вы со своим онанизмом и бездушными вычислениями на мертвых машинах всё портите! DEUS VULT!

Ответы193711937741025

13 30 мая 2017, 01:08 13 19371

>>19368
Ага, двачую, только я вот стыжусь почему-то об этом писать.

Ответы1938719405

71 Кб, 590x374
14 30 мая 2017, 10:54 14 19377

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

Ответы19405

15 30 мая 2017, 15:07 15 19387

>>19371
И правильно делаешь

16 31 мая 2017, 00:31 16 19405

>>19377
Разумеется, я лишь merely компиляю-пересказываю того же Канта.
>слон
Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообще?

>>19371
>Стыд
Самое глупое из человеческих чувств.

Ответы1945319534

17 31 мая 2017, 16:19 17 19453

>>19405
> Так говоришь, будто ты со стороны видишь всю математику, и подшучиваешь над слепцами, которые то доказывают что-то с помощью ЭВМ, то рассуждают интуитивно.
> Но это наверняка не так, и вполне уместен вопрос: а имеет ли смысл говорить о «слоне» вообщ
Я как раз думаю, что нашел нечто интересное, позволяющее связать эти подходы. Нет, не узоры с разрывами.

18 1 июня 2017, 18:00 18 19534

>>19405
>Самое глупое из человеческих чувств.
Ну это интимное ведь, ты же голым не ходишь по улице.

19 2 июня 2017, 10:35 19 19581

>>19366

Я переключился на библиотеку ZFC в Metamath. NBG тоже вполне можно лаконично на метамаф реализовывать. (пока нет такой задачи, не нужно)

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

В целом - потрясающей красоты вещь, я в восторге.

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

20 16 янв 2018, 02:30 20 34990

>>19355

про пункт 3)
да, выразимо.
Но теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Как раз metamath подходит.

Ответы35144

21 16 янв 2018, 06:53 21 34994

>>19319 (OP)
Ого, тред еще живой.

22 16 янв 2018, 22:23 22 35144

>>34990
> теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Лямбда же. Ну и изоморфизм Карри-Говарда. В конечном счёте все обоснование упирается в вычислимость. Как и MLTT.

Ответы35177

23 17 янв 2018, 13:44 23 35177

>>35144
Если ты из Москвы, то давай увидимся в НМУ 20го января в 13:00 ? Там книжный хороший, тебе понравится, как раз туда собираюсь.

24 26 июня 2018, 21:31 24 41025

>>19368
>Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности.
Вы сильно преувеличиваете. Математика — это просто описание некоторых аспектов реальности, вот и всё. Нет никакого "более глубокого" познания. Всё познание одинаковое.

Ответы4103241038

25 26 июня 2018, 22:33 25 41032

>>41025
пиздец ты некрофил

sage 26 27 июня 2018, 11:11 26 41038

>>41025
тред же про метамаф... не надо тут, я хотел бы, чтобы последним постом было следующее заключение:

1) там очень сомнительная и некрасивая теория типов.
2) Язык слишком бедный
3) В такого рода системах можно легко нарваться на противоречие. ( из-за того, что там замены без нормального вывода типа)
4) Морока с "различностью переменных" - излишняя грузящая синтаксис вещь.

Поэтому пусть этот тред утонет: есть куда более красивые и полезные аналогичные классические вещи - элементарные теории первого порядка.

ОП

Тред закрытОбновить закрытый тред
« /math/В начало тредаВеб-версияНастройки/a//b//mu//s//vg/Все доски

Скачать тред только с превьюс превью и прикрепленными файлами

Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах.Подробнее

Пользуетесь скринридером — пишите, что можно улучшить.
Host-Food.ru — надёжный хостинг от 12 руб/мес | Free DNS
Зеркала М.Двача: m2ch.hk, m2ch.lib, m2chfapiswfw2wcakptqp4o6ltgchvjuxfab7urxlduraomtlnhw5xad.onion