![](http://webcf.waybackmachine.org/web/20210511135229im_/https://habrastorage.org/getpro/habr/avatars/29c/ef2/4f8/29cef24f873b4c2f2bdf1d3ada13e9b9.png)
Управление робототехникой в реальном времени с помощью языка Lean
- Блог компании SkillFactory,
- Функциональное программирование,
- Разработка робототехники,
- Разработка под Arduino,
- Робототехника
- Перевод
![](https://webcf.waybackmachine.org/web/20210511135229im_/https://habrastorage.org/getpro/habr/upload_files/ea0/05d/36a/ea005d36a31805182d402a384ce9d704.png)
Подразделение Microsoft Research недавно опубликовало предварительный выпуск Lean 4. Предыдущие версии Lean были сосредоточены на том, чтобы быть помощником по доказательствам — программным инструментом, который облегчает разработку строгих математических доказательств с помощью интерактивной совместной работы человека и машины. До сих пор язык Lean в основном применялся для оцифровки теоретической математики.