s
Господа, вы переизобретаете типы.
Size: a a a
2021 November 16
s
X
с одной стороны, этот друг раньше отметился проблемами с пониманием конечномерной линейной алгебры на уровне +- конспектов письменного
X
и кидать ему ссылки на теоркат и теорию типов — ну хз, жестоко
X
но с другой стороны — возможно как раз тот случай, когда неплохо бы, чтобы такая вещь, как де морган, зашла в подкорку плотно, прочно, и по возможности с очень хорошо доступным выводом
s
По мне, так несколько правил вывода и немного практики, и такие вещи перестают быть проблемой.
s
И если использовать интерактивный прувер, то даже в голове ничего держать не нужно.
s
Он на каждом шаге тебе показывает, что осталось доказать.
s
Мы живём во времена, когда mathlib существует, а люди формализуют нетривиальные вещи.
BV
Mathlib какого ЯП?
s
И стоит хотя бы немного уметь пользоваться такими инструментами.
X
ты, кхм, take too much for granted
s
Lean.
BV
Не знаю такого, вот честно
X
есть стойкое ощущение, что этот человек посмотрит на трёхчленный силлогизм, и останется с вопросом, почему утверждение верно.
X
то есть там проблема оч глубока
s
s
В общем, вокруг Lean неплохое такое сообщество математиков собралось.