Каково ваше мнение о https://proofcheck.org? Это cmd-инструмент, который позволяет проверять TEX-овые доказательства на математическую (!) корректность. Но на русском статей о нём нет, хотя он прост в использовании и по своему принципу функционирования. Прилагаю также proof-of-concept от авторов: https://tug.org/TUGboat/tb30-2/tb95neveln.pdf
Суть в том, что до этого существовало много proof assistant-ов, но эти предложили принципиально новый стандарт парсинга логики, который уложился в скрипт на питоне. В отличие от семейства HOL, основные идеи которого восходят аж к 1970-м. Я считаю, что нужно популяризировать ProofCheck и в рунете.
Authors' contribution
jemmybutton 256.8habrahabr 184.0Alex_Novosib 126.0m1rko 119.6Skiminok 97.0mmatrosov 76.0Amet13 75.0raliev 73.0kotomanov 73.0