Оглавление
Lean (помощник по проверке)
-
Обзор Lean
- Lean – это инструмент для верстки и функциональный язык программирования.
- Основан на индуктивных типах и имеет открытый исходный код на GitHub.
- Разработан Леонардо де Моурой и поддерживается некоммерческой организацией FRO.
-
История и развитие
- Lean был запущен в Microsoft Research в 2013 году, с экспериментальными версиями и отказом от некоторых функций.
- Lean 3, выпущенная в 2017 году, была первой стабильной версией, реализованной в основном на C++, с некоторыми функциями на самом языке Lean.
- После версии 3.4.2 началась разработка Lean 4, а сообщество выпустило неофициальные версии до 3.51.1.
- Lean 4, выпущенный в 2021 году, переосмыслил программу доказательства теорем и добавил систему макросов и улучшенные процедуры.
- Lean 4 не совместим с Lean 3 и не имеет обратной совместимости.
-
Обзор библиотек и интеграции
- Lean включает стандартную библиотеку std4 и проект mathlib для оцифровки чистой математики.
- Lean интегрируется с различными редакторами, включая Code Visual Studio и Emacs, и поддерживает Unicode.
- Lean может быть скомпилирован на JavaScript и доступен в веб-браузере.
-
Примеры и использование
- Lean используется математиками для формализации теорем и доказательств, включая проект Xena.
- OpenAI и Meta AI создали модели искусственного интеллекта для решения математических задач на языке Lean.
-
Дополнительные ресурсы
- Ссылки на математический портал, портал бесплатного программного обеспечения с открытым исходным кодом и другие связанные темы.
Полный текст статьи: