Интерактивная система доказательства математических теорем на Python с кликабельным интерфейсом вместо кода.
pyHOL — переработанная версия проекта holpy: доказательство теорем в логике высшего порядка, где пользователь строит доказательства кликами, а не пишет формальный язык вручную. В основе лежит проверенное ядро в стиле LCF, каждый шаг доказательства можно независимо перепроверить; есть веб-интерфейс с IDE для доказательств и верификации программ, а также подробное руководство из семи глав.
Описание автора:An interactive HOL theorem prover in Python
Python★ 0создан 21 сентября 2026форков 0BSD-3-Clause