Четыре ведущих ассистента доказательств получили стандартизированные бенчмарки

Представлены нормализованные тесты для сравнения эффективности четырёх популярных ассистентов доказательств: Agda, Idris, Lean и Coq (Rocq). Бенчмарки написаны на DSL и транслируются в целевые языки, что позволяет объективно оценить их производительность.