ГG
Кому не нужен?
Size: a a a
2021 November 29
V🇺
кожаные мешки не нужны
a
Да, программированию можно сильно легче научиться в одиночку из-за более высокой интерактивности, и эту интерактивность было бы здорово получить в математике. Я б хотел писать такие инструменты. Но вот пруверы в их нынешнем виде меня не привлекают совсем.
s
на самом деле это не так, переходя на следующий блок, становится или не понятно, или доказательства не сходятся, то есть к мнимым числам я вернулся из за интегралов
s
А к множествам не вернулся.
s
А если бы использовал прувер, то застрял бы ещё на множествах до того момента, пока бы их как следует не понял.
ГG
А как вы от интегралов вернулись к комплексным?
a
Хитрый не гомотопный геодезической путь, ведущий от интегралов через комплексные числа в бан.
V🇺
чтобы понимать код для пруфера - уже нужен нехилый фундамент, если честно
BV
а может даже и не только он
V🇺
как минимум ещё умение отделять суть доказательства от несущественных технических деталей
s
На самом деле нет.
V🇺
хорошо так говорить, когда фундамент уже есть
BV
хорошо(с)
s
Правила вывода это очень механическая вещь.
s
И во многом прувер напоминает язык программирования, просто с более выразительными типами.
V🇺
ассемблер - тоже очень механическая вещь, но читать его без подготовки в CS - гиблое дело
BV
когда ты знаешь их и используешь на уровне интуиции
s
Но люди читают.
BV
кто знает те читают