(Это связано с основаниями математики, но не спешите отчаиваться)
В данном треде я постараюсь ответить на все возникшие у анонов вопросы. Его вроде надо сделать модерируемым.
FAQ:
1)Что это?
Это теория типов для формального доказательств первопорядковых языков. Ну то есть язык программирования для ZFC, NBG, геометрии (Тарского) и ещё много чего первопорядкового.
Всё это доступно онлайн в удобном гипертекстовом виде.
2)Какие профиты?
а) Очень большая библиотека доказательств, легко читается. Имеет достаточно долгую историю - с девяностых.
б) Пруфассистант: два режима, как в Coq: либо конструируешь доказательство, либо интерактивный режим.
в) Непосредственно прилагается самоучитель.
г) Простой (300 строк на питоне) верификатор доказательств.
д) Имеет модель в ZFC. (самая мякотка, смотри пункт 3)
е) Живое коммьюнити.
3) Какие задачи?
Есть такая статья: http://us.metamath.org/ocat/model/model.pdf
Не знаю как анону, но мне было бы очень любопытно в ней разобраться.
4) Почему "лучше" чем HoTT, Coq, HOL и т.д.?
Да потому что ZFC и логика предикатов - это математический стандарт де-факто, поэтому знание metamath может помочь вам понимать беглую речь преподавателей в институте. (А не страдать по крайностям "это очевидно" и "ничерта не понятно".)
Смело задавайте вопросы и высказывайте мнения.
Пропущено 21 постов, 6 с картинками.
> теорию стоящую за коком тоже надо как-то обосновать. В чём-то простом.
Лямбда же. Ну и изоморфизм Карри-Говарда. В конечном счёте все обоснование упирается в вычислимость. Как и MLTT.
Если ты из Москвы, то давай увидимся в НМУ 20го января в 13:00 ? Там книжный хороший, тебе понравится, как раз туда собираюсь.
>Математика - это заложенный самим Богом способ более глубокого, чем обыденное, познания окружающей действительности.
Вы сильно преувеличиваете. Математика — это просто описание некоторых аспектов реальности, вот и всё. Нет никакого "более глубокого" познания. Всё познание одинаковое.
тред же про метамаф... не надо тут, я хотел бы, чтобы последним постом было следующее заключение:
1) там очень сомнительная и некрасивая теория типов.
2) Язык слишком бедный
3) В такого рода системах можно легко нарваться на противоречие. ( из-за того, что там замены без нормального вывода типа)
4) Морока с "различностью переменных" - излишняя грузящая синтаксис вещь.
Поэтому пусть этот тред утонет: есть куда более красивые и полезные аналогичные классические вещи - элементарные теории первого порядка.
ОП
Пропущено 5 постов, 1 с картинками.
∆
∆ ∆
>саня хуй саси
Предыдущий - https://2ch.hk/math/res/21361.html
Пропущено 518 постов, 59 с картинками.
Почти. Видимо корректнее будет сформулировать как то, что математика, программирование и теория типов - это одно и тоже.
А нельзя ли как-нибудь это индукцией доказать?
Или кококтивисты ее тоже не используют?
>В любой математике ровно столько математики, сколько в ней вычислимости.
Предыдущий, тонет тут: https://2ch.hk/math/res/25624.html
Архивач: https://arhivach.cf/thread/369697/ (У кого не открывается - попробуйте HTTP.)
Перекат: https://2ch.hk/math/res/40955.html
Перекат: http://arhivach.cf/thread/369744/
Перекат: >>40955 (OP)
Перекот: https://2ch.hk/math/res/40955.html
Перекот: http://arhivach.cf/thread/369744/
Перекот: >>40955 (OP)
Перекіт: https://2ch.hk/math/res/40955.html
Перекіт: http://arhivach.cf/thread/369744/
Перекіт: >>40955 (OP)
>>40381
>Браузер писал, то так оно и есть. Слово Браузера - закон.
Вот это было излишне, ибо на принципах интерпретатора:
>>40466
>непогрешимость браузера ещё сильнее усилилась
Столкнулся с проблемой, что начав изучать школьную программ, я в принципе могу решать задачки и всю прочую хуйню, ноя не понимаю, что делаю. Взять даже квадратное уравнение и нахождение дискриминанта: я помню формулу, но не могу сказать, что она значит и откуда она вообще взялась. Моё "математическое" мышление на данный момент строится лишь на некотором количестве заученных формул, большую часть которых я даже не смогу доказать.
Чтобы начать понимать математику, стоит ли мне обмазаться учебниками логики или не выёбываться и просто сидеть решать всякую хуйню 24/7, а понимание придёт само?
Пропущено 5 постов, 1 с картинками.
Математика дает тебе и логику и мышление и систему и хорошее настроение. А логика дает только логику, делай выводы.
Не слушай троля выше. То, что ты называешь логикой - не имеет учебников, потому что там одно два логических следствия, к которым нужно привыкнуть. Все учебники по логике - это учебники по конкретной ветве науки, которая, вообще говоря, довольно сложная.
Все что тебе нужно это осознание пары очевидных фактов и простейшая теория множеств, типа объединения, пересечения, и отрицания.
Но на самом деле я тебя обманул и тебе это не нужно. А что же нужно&?
1. Перестать быть пиздоглазым мудилом и не создавать тред, блять, а пойти в загон для начинающих. Ебанутый, в закрпленном треде написано. ты вообще дебил? Думаешь ты первый, кто испытывает проблемы со школьной математикой?
2. Послать на хуй своего учителя или учебник. Если ты не знаешь вывод теорем, то это значит, что либо ты ленивый бич, который не хочет их узнавать, либо тебе их банально не дали. Как узнать то, чего тебе не дают. Я подозреваю, что у тебя второе. Выбери любую книжку по школьной математике, список есть в соседнем треде, оюходи стороной историю математики и философию. Реально, беги как от огня, а адептов не считай людьми.
В примере с уравнением квадратным. Что значит
>но не могу сказать, что она значит
Формула - это как форма на сайте, вставляешь свои значения и получаешь ответ, что ты, вроде как, умеешь.
Что касется вывода. Нужно выделить полный квадрат, и дальше эта формула вылезет. Это не очень трудно, но и не быстро ,поэтому эту формулу и учат, чтобы каждый раз не выводить. а именно такой вид она имеет потому, что нужно выделить именно дискриминант, на нем все и может сломаться, остальные же действия надежны как часы. Ну кроме деления на а, но там изначальное условие помогает.
Итак, резюмируя.
>стоит ли мне обмазаться учебниками логики
Нет, не стоит.
>не выёбываться и просто сидеть решать всякую хуйню 24/7
Это тоже вариант, в конце концов догадаться до решение квадратного уравнения не очень сложно. Но гораздно проще и быстрее посмотреть решение в учебнике или спросить тут.
В старших классах будут производные, в этом случае тебе придется либо просто выучить, либо искать хороший источник, где объяснят вывод всех этих формул. Проблема в том, что в школе не рассказывают строго, что такое производная.
>Деды конечно уверяют, что это развивает интуицию, телепатические способности и улучшает потенцию, но это не так.
Почему диды такие крутые?
У них есть все - свой дхду, свои люди в министерстве образования, физики их уважают, а гуманитарии им завидуют. От одного слова "матан" случайные прохожие разбегаются в благоговейном трепете, а при слове "пучки" люди только зовут модератора с формулировкой "несовершеннолетний". Пока неудачники кучкуются в каких-то подпольных клубах типа НМУ и носятся со своими листочками, деды возглавляют лучшие вузы страны. У них есть все: деньги, власть, уважение. Даже лоли у них есть. Про них снимают фильмы, а про тебя через 10 лет не вспомнит даже конструктивный петух.
Картофан - это успех. Деды - это сила. Война проиграна, господа.