Андрій Севастьянов пояснює, як математичні доведення можна записати у вигляді коду в мові програмування Lean 4. 

У статті про те, чому мова для цього не може бути Т'юрінг-повною, що таке структурна рекурсія та залежні типи і як на практиці працює ізоморфізм Каррі — Говарда.

 [https://dou.ua/goto/6jKN](https://dou.ua/goto/6jKN)