fp atp programming Хочу на летних каникулах познакомиться с зависимыми типами и ATP. Я не математик, поэтому просто на побаловаться. Никаких знаний о возможностях пруверов у меня сейчас нет. Насколько они применимы, например, к таким прикладным разделам математики, как линейная алгебра, теория групп и т.п? Есть ли какие-то "библиотеки" для этого дела?
И что выбрать: Idris, Agda, Coq?