Сравнение четырёх доказателей теорем: Isabelle/HOL, Lean, HOL4 и Agda

Статья представляет сравнительный анализ четырёх популярных систем интерактивного доказательства теорем. Рассматриваются особенности Isabelle/HOL, Lean, HOL4 и Agda с авторской позицией по их применимости.