Leanin: библиотека конкурентности для Lean 4, вдохновлённая Tokio, с формально верифицированными доказательствами

Представлена библиотека Leanin, реализующая модели конкурентного программирования по аналогии с Rust-фреймворком Tokio, но для языка доказательств теорем Lean 4. Особенность проекта заключается в наличии машинно-проверяемых доказательств корректности, что обеспечивает высокий уровень надёжности при работе с параллельными вычислениями.