Пропущено 48 постов, 5 с картинками.
Лютая годнота, анон
Смотрел со своим кунчиком. Такая скучнота, что дважды поняшились.
Постиронии тред го
Гугл сломался? Изучаешь анатомию (надо купить труп, формалин), гистологию (препараты животных, микроскоп), микробиологию, биохимию, нормальную физиологию. Как изучишь приходи.
На самом деле это очень важная проблема и очень большое упущение в нашей (общечеловеческой в том числе) системе образования. Я понимаю твою иронию, но на самом деле получать столько же знаний, как у выпускника меда, совсем не нужно, если ты не деньги этим зарабатывать собрался. А вот основы здорового образа жизни и самопомощи - это, быть может, вообще самое важное, чему могут научить ребенка в школе. Но не учат. Даже предмет у них есть: физическая культура. Вот только никакой культуры там не преподают.
и да, я про медицину, а не про математикуначувствуются своей постиронией и ябут друг друга в жопы
Не спешите гнать в философач. Я попытался обмазаться (чисто ради примитивной эрудиции), и мне подумалось, что в образе мысли есть что-то перекликающееся с теорией категорий. Такая мысль пришла от чтения этой книги:
https://ru.wikipedia.org/wiki/Сефер_ха-Зоар
Пропущено 39 постов, 7 с картинками.
Ой, почти случайно увидел тебя. Ты читаешь мои гугло-запросы? Или тебе так сказали ранее?
У меня чё-то Каббала ассоциируется с кредитным рабством,
и я даже знаю почему - а именно, по ключевому слову "закаббалить".
Но на самом-то деле это не так.
Она с Торой связана, а там канон Ветхого Завета, который на уровне фундаментализма,
и Иудейский, и Православный, и Католический (и Христианский вцелом).
https://ru.wikipedia.org/wiki/Ветхий_Завет#Канон_Ветхого_Завета
Но я ничего не понимаю там. Я по диагонали читал.
Я не думаю, что надо в этом разбираться, и как-либо интерпретировать,
ведь это всё можно запрограммировать - наилучшим образом.
В настоящей науке нет чего-то 100%ного, она строится на подтверждающихся теориях, которые могут быть не точны или неприменимы в других областях(что не уменьшает её важности). Например та же классическая физика Ньютона, которая оказалась неприменима к свету(что потом разрулил Эйнштейн наше всё, но не в микромире) Наука достаточно достоверна, но её достижения не абсолютны, понимаешь? Но это не отменят того факта, что научный метод - самый точный и достоверный источник знаний
Кстати, по 100% процентов как раз таки и заливают всякие религиозники, а труъ учёные просто занимаются своим делом. и их результаты не всегда точны на все сто, что они и сами признают (я уже говорил, что ньютоновскую физику пришлось "корректировать")
(Это связано с основаниями математики, но не спешите отчаиваться)
В данном треде я постараюсь ответить на все возникшие у анонов вопросы. Его вроде надо сделать модерируемым.
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) Морока с "различностью переменных" - излишняя грузящая синтаксис вещь.
Поэтому пусть этот тред утонет: есть куда более красивые и полезные аналогичные классические вещи - элементарные теории первого порядка.
ОП