|
|
Я - не матетематик, я мог бы ответить на похожий вопрос вроде "зачем Rust есть же C". Попробую ответить с точки зрения досужего наблюдателя. Lean новее и его автор, вероятно, хорошо знаком с Coq - однако, решил идти своим путём. Есть достаточно много сайтов, где различия обсуждаются в деталях. Мой вывод по беглому просмотру - главное отличие в более крупном и энергичном сообществе вокруг Lean, которое создало и пополняет mathlib (единый репозиторий накопленных формализаций - похоже, аналогичного такого же богатого репозитория на Coq нет).
(Читать комментарии) Добавить комментарий:
|
|